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 768  ax11i 1134  ax11eq 1356  ax11el 1357  eleq1a 1535  ceqsalg 1816  cgsexg 1822  cgsex2g 1823  cgsex4g 1824  ceqsex 1825  cla42egv 1855  cla43egv 1857  ralxfr 2889  iunpw 2904  onfr 2976  ordun 3071  funcnvuni 3550  funfvop 3788  cbvfo 3870  abianfp 3947  oaordex 4176  ecelqsi 4276  eceqopreq 4297  fundmen 4409  nneneq 4492  unfilem1 4524  ac6lem 4726  zorn2lem3 4762  zorn2lem7 4766  ltrpq 5057  genpnnp 5080  ltaddpr 5112  reclem3pr 5130  reclem4pr 5131  suppsrlem 5193  suppsr3 5196  suprelem 5231  elfz4t 6407  abslt 6810  absle 6811  absltOLD 6812  absleOLD 6813  cau2 6850  fsum1 6943  ser1clim0 7109  unctb 7519  cnsscnp 7711  nmoubi 8367  nmopubt 9749  nmfnleubt 9765  mdbr3 10134  mdbr4 10135  atssmat 10213  atcvatlem 10220  uninqs 10342  hmphre 10417  iintlem1 10476  mrdmcd 10566

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