Theorem biimpcd 137

Description: Deduce a commuted implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpd.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpcd	|- (ps -> (ph -> ch))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		biimpd.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 135	. 2 |- (ph -> (ps -> ch))
3	2	com12 13	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  biimpac 326  clneq 1168  clneq2 1169  psssstr 1576  disjsn 1836  tz7.7 2224  limsssuc 2362  nnsuc 2389  peano5 2394  tz6.12c 2846  chfnrn 2885  ffnfv 2892  cbvfo 2923  oawordexr 3158  ereldm 3222  eceqopreq 3249  pssnn 3428  zornlem6 3608  fodomb 3615  prub 3892  prnmadd 3894  prlem936 3949  letrt 4291  chocuni 5179  pjpj0 5259  5oalem6 5549  atcvatlem 5770  mdsymlem3 5778

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org