Theorem biimprcd 138

Description: Deduce a converse commuted implication from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimprcd

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

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

This theorem is referenced by:  biimparc 327  prlem1 576  eleq1a 1158  ceqsalg 1362  cgsex2g 1368  cgsex4g 1369  ceqsex 1370  cla4e2gv 1398  sbcie 1455  iunpw 2040  onfr 2237  ordun 2332  funcnvuni 2706  funopfv 2886  cbvfo 2923  abianfp 3000  oaordex 3160  ecelqsi 3229  eceqopreq 3249  fundmen 3333  nneneq 3408  unfilem1 3438  ac6lem 3575  zornlem3 3605  zornlem7 3609  ltrpq 3879  genpnnp 3902  ltaddpr 3934  reclem3pr 3952  reclem4pr 3953  suppsrlem 4015  suppsr3 4018  suprelem 4053  sup2 4510  abslt 4855  absle 4856  mdbr3 5729  mdbr4 5730  atcvatlem 5770

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