Theorem biimprcd 156

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 154	. 2 |- (ph -> (ch -> ps))
3	2	com12 11	1 |- (ch -> (ph -> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  biimparc 419  prlem1 769  ax11i 1136  ax11eq 1361  ax11el 1362  eleq1a 1540  ceqsalg 1821  cgsexg 1827  cgsex2g 1828  cgsex4g 1829  ceqsex 1830  cla42egv 1860  cla43egv 1862  ralxfr 2894  iunpw 2909  onfr 2981  ordun 3076  funcnvuni 3556  funfvop 3794  cbvfo 3876  abianfp 3953  oaordex 4182  ecelqsi 4282  eceqopreq 4303  fundmen 4415  nneneq 4498  unfilem1 4530  ac6lem 4734  zorn2lem3 4770  zorn2lem7 4774  ltrpq 5065  genpnnp 5088  ltaddpr 5120  reclem3pr 5138  reclem4pr 5139  suppsrlem 5201  suppsr3 5204  suprelem 5239  elfz4t 6415  abslt 6818  absle 6819  absltOLD 6820  absleOLD 6821  cau2 6858  fsum1 6951  ser1clim0 7117  unctb 7527  cnsscnp 7722  nmoubi 8380  nmopubt 9772  nmfnleubt 9788  mdbr3 10162  mdbr4 10163  atssmat 10242  atcvatlem 10249  uninqs 10378  hmphre 10453  iintlem1 10512  mrdmcd 10602

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain