Theorem biimpcd 155

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

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

This theorem is referenced by:  biimpac 420  nbn2 725  ax16 1215  ax16i 1276  nelneq 1568  nelneq2 1569  psssstr 2161  disjsn 2451  mosubopt 2818  tz7.7 2987  limsssuc 3135  nnsuc 3162  peano5 3167  asymref2 3454  ssimaex 3782  chfnrn 3816  ffnfv 3842  cbvfo 3899  elopabi 4131  eloprabi 4132  odi 4224  ereldm 4299  eceqopreq 4327  pssnn 4549  zorn2lem6 4805  alephval3 4916  prub 5111  prnmadd 5113  prlem936 5168  letrt 5538  ssxr 5553  xrletrt 5577  snunioolem 6364  facwordit 6958  climsup 7169  dscmet 7927  pjpj0 9262  5oalem6 9611  eigorth 9770  adjbd1o 10025  atcvatlem 10320  mdsymlem3 10340  dmdbr7at 10359  fiiu 10457  fiiu2 10492  hmeobc 10548  fgsb 10575  fgsb2 10580  eloi 10650

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