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 721  ax16 1209  ax16i 1270  nelneq 1561  nelneq2 1562  psssstr 2152  disjsn 2441  mosubopt 2804  tz7.7 2973  limsssuc 3121  nnsuc 3148  peano5 3153  asymref2 3440  ssimaex 3768  chfnrn 3802  ffnfv 3828  cbvfo 3885  elopabi 4117  eloprabi 4118  odi 4210  ereldm 4285  eceqopreq 4313  pssnn 4534  zorn2lem6 4793  alephval3 4903  prub 5098  prnmadd 5100  prlem936 5155  letrt 5525  ssxr 5540  xrletrt 5564  snunioolem 6414  facwordit 6944  climsup 7155  dscmet 7918  pjpj0 9255  5oalem6 9604  eigorth 9763  adjbd1o 10018  atcvatlem 10312  mdsymlem3 10332  dmdbr7at 10351  fiiu 10453  fiiuOLD 10454  fiiu2 10488  fiiu2OLD 10489  hmeobc 10542  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfillem2OLD 10588  eloi 10659

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