Theorem biimpcd 153

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

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

This theorem is referenced by:  biimpac 418  nbn2 726  ax16 1246  ax16i 1308  nelneq 1604  nelneq2 1605  psssstr 2204  disjsn 2502  mosubopt 2881  tz7.7 3001  limsssuc 3204  nnsuc 3235  peano5 3241  asymref2 3532  ssimaex 3879  chfnrn 3916  ffnfv 3942  cbvfo 3999  elopabi 4179  eloprabi 4180  odi 4346  ereldm 4425  eceqopreq 4454  pssnn 4681  zorn2lem6 4939  alephval3 5053  prub 5252  prnmadd 5254  prlem936 5309  letr 5679  ssxr 5694  xrletr 5718  snunioolem 6541  facwordi 7147  climsupi 7358  dscmet 8129  pjpj0i 9531  5oalem6 9882  eigorthi 10043  adjbd1o 10297  atcvatlem 10594  mdsymlem3 10614  dmdbr7ati 10633  fiiu 10738  ref3w 10772  mlteqer 10789  eloi 10817  fiiu2 10852  ismgm 10897  ismnd2 10928  hmeobc 11048  fgsb 11082  fgsb2 11086  altretoplem2 11143  fiuni 11420  elfiun 11421  alexsublem2 11497  1stcclb 11532  filssufillem 11655  filcon 11665  isga 11772  f1elima 11818  dif1card 11835  inficl 11849  sstotbnd 11992  heiborlem10 12020  heiborlem11 12021  heiborlem13 12023  heiborlem29 12039  heiborlem41 12051

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 145

Copyright terms: Public domain