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 418  nbn2 720  ax16 1207  ax16i 1268  nelneq 1558  nelneq2 1559  psssstr 2148  disjsn 2437  mosubopt 2799  tz7.7 2968  limsssuc 3116  nnsuc 3143  peano5 3148  asymref2 3432  ssimaex 3759  chfnrn 3793  ffnfv 3819  cbvfo 3876  elopabi 4107  eloprabi 4108  odi 4200  ereldm 4275  eceqopreq 4303  pssnn 4519  zorn2lem6 4773  alephval3 4883  prub 5078  prnmadd 5080  prlem936 5135  letrt 5506  ssxr 5521  xrletrt 5545  snunioolem 6355  facwordit 6889  climsup 7099  dscmet 7870  pjpj0 9193  5oalem6 9544  eigorth 9703  adjbd1o 9956  atcvatlem 10249  mdsymlem3 10269  fiiu 10386  fiiu2 10413  fgsb 10480  fgsb2 10485  eloi 10539

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