Theorem biimpcd 172

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

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

This theorem is referenced by:  biimpac 462  nbn2 790  3impexp 1286  3impexpbicom 1287  ax16 1579  ax16i 1647  nelneq 1985  nelneq2 1986  nelne 2100  psssstr 2716  disjsnOLD 3090  difsn 3125  mosubopt 3551  tz7.7 3684  limsssuc 3934  nnsuc 3969  peano5 3975  asymref2OLD 4311  ssimaex 4729  chfnrn 4775  ffnfv 4801  cbvfo 4861  elopabi 5059  eloprabi 5060  odi 5258  ereldm 5343  eceqopreq 5372  pssnn 5628  sbcim2g 5841  zorn2lem6 5955  alephval3 6051  prub 6250  prnmadd 6252  prlem936 6307  letr 6695  ssxrOLD 6715  xrletr 6739  snunioolem 7583  facwordi 8196  climsupi 8415  dscmet 9196  isga 9450  dif1card 10177  fiuni 10219  fiiu2 10220  hmeobc 10239  ismgm 10367  ismnd2 10392  pjpj0i 10888  5oalem6 11239  eigorthi 11400  adjbd1o 11655  atcvatlem 11957  mdsymlem3 11977  dmdbr7ati 11996  isprm2 13775  coprm 13782  fundmpss 13836  ordsucuniel 13863  axbday 14012  axfelem16 14046  axfelem17 14047  altopelaltxp 14099  fnoprvpop 14338  fiiu 14344  ref4w 14370  eloi 14400  repcpwti 14503  prjmapcp2 14515  nZdef 14527  cur1vald 14547  dutos1 14626  ltlga 14729  fgsb 14921  fgsb2 14925  altretoplem2 14996  mlteqer 15017  lvsovso 15038  dualcat2 15133  isline1 15294  elfiun 15369  alexsublem2 15438  1stcclb 15471  filssufillem 15570  filcon 15580  f1elima 15719  inficl 15757  fdc1 15813  sstotbnd 15936  heiborlem10 15964  heiborlem11 15965  heiborlem13 15967  heiborlem29 15983  heiborlem41 15995  suctrALT2VD 16660  suctrALT2 16661  3impexpVD 16680  3impexpbicomVD 16681  sbcim2gVD 16699  pltletr 16791  atomnle 17016  hl2atom 17053  cvratlem 17061  ispsubcl2 17356

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 164

Copyright terms: Public domain