Theorem biimpcd 228

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimpcd	|- ( ps -> ( ph -> ch ) )

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ps -> ps )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibcom 224	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   <-> wb 188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 189

This theorem is referenced by:  biimpac  489  axc16i  2156  nelneq  2553  nelneq2  2554  nelne1  2720  nelne2  2721  nssne1  3488  nssne2  3489  psssstr  3539  difsn  4106  iununi  4366  disjiun  4393  nbrne1  4420  nbrne2  4421  mosubopt  4699  issref  5213  tz7.7  5449  tz6.12i  5885  ssimaex  5930  chfnrn  5993  fvn0ssdmfun  6013  ffnfv  6049  f1elima  6164  elovmpt3rab1  6527  limsssuc  6677  nnsuc  6709  peano5  6716  dftpos4  6992  odi  7280  fineqvlem  7786  pssnn  7790  ordunifi  7821  wdom2d  8095  r1pwss  8255  alephval3  8541  infdif  8639  cff1  8688  cofsmo  8699  axdc3lem2  8881  zorn2lem6  8931  cfpwsdom  9009  prub  9419  prnmadd  9422  1re  9642  letr  9727  dedekindle  9798  addid1  9813  negf1o  10049  negfi  10554  xrletr  11455  0fz1  11819  elfzmlbp  11902  leisorel  12623  elss2prb  12643  exprelprel  12646  fi1uzind  12650  swrdnd  12788  swrdccatfn  12838  sqrmo  13315  dvdseq  14352  isprm2  14632  nprmdvds1  14650  catsubcat  15744  funcestrcsetclem8  16032  funcestrcsetclem9  16033  fthestrcsetc  16035  fullestrcsetc  16036  funcsetcestrclem9  16048  fthsetcestrc  16050  fullsetcestrc  16051  pltletr  16217  mgm2nsgrplem3  16654  sgrp2nmndlem3  16659  fvcosymgeq  17070  sylow2alem2  17270  islss  18158  assamulgscmlem2  18573  gsumply1subr  18827  gzrngunitlem  19032  pjdm2  19274  dmatmul  19522  decpmatmullem  19795  monmat2matmon  19848  chpscmat  19866  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  isclo2  20104  fbasfip  20883  ufileu  20934  alexsubALTlem2  21063  cnextcn  21082  metustbl  21581  usgrarnedg1  25116  nbgraf1olem3  25171  nbgraf1olem5  25173  nb3graprlem1  25179  cusgrafilem2  25208  wlkn0  25255  fargshiftfo  25366  3v3e3cycl1  25372  4cycl4v4e  25394  4cycl4dv4e  25396  wlkiswwlk2lem3  25421  wlklniswwlkn1  25427  wlklniswwlkn2  25428  wwlknext  25452  clwwlknimp  25504  clwlkisclwwlklem2a1  25507  clwlkisclwwlklem2a  25513  clwwlkel  25521  clwwlkext2edg  25530  wwlkext2clwwlk  25531  clwwisshclwwlem  25534  hashecclwwlkn1  25562  usghashecclwwlk  25563  clwlkfclwwlk  25572  clwlkf1clwwlklem2  25575  el2wlkonot  25597  el2wlkonotot1  25602  frgrancvvdeqlemA  25765  frgrancvvdeqlemC  25767  frgraeu  25782  numclwlk2lem2f  25831  numclwlk2lem2f1o  25833  frgraogt3nreg  25848  ismgmOLD  26048  5oalem6  27312  eigorthi  27490  adjbd1o  27738  dmdbr7ati  28077  dfpo2  30395  fundmpss  30407  funbreq  30411  idinside  30851  bj-eldiag2  31647  poimirlem32  31972  sdclem2  32071  fdc1  32075  lsatcvatlem  32615  atnle  32883  cvratlem  32986  ispsubcl2N  33512  trlord  34136  diaelrnN  34613  cdlemm10N  34686  dochexmidlem7  35034  3impexpbicom  36834  sbcim2g  36899  suctrALT2VD  37232  suctrALT2  37233  3impexpVD  37252  3impexpbicomVD  37253  sbcim2gVD  37272  csbeq2gVD  37289  csbsngVD  37290  ax6e2ndeqVD  37306  2sb5ndVD  37307  lptioo2  37711  lptioo1  37712  funressnfv  38629  ffnafv  38673  iccpartiltu  38736  iccpartigtl  38737  icceuelpartlem  38749  oddprmuzge3  38841  bgoldbtbndlem2  38901  propeqop  38999  ushgredgedga  39306  ushgredgedgaloop  39308  nbgrval  39406  edgnbusgreu  39441  nb3grprlem1  39454  cusgrfilem1  39516  cusgrfilem2  39517  uspgrloopvtxel  39554  umgr2v2evtxel  39559  1wlkn0  39636  1wlkcompim  39644  usgedgimp  39768  usgedgimpALT  39771  fusgraimpcl  39792  fusgraimpclALT  39794  fusgraimpclALT2  39796  mgmpropd  39828  rngcinv  40036  rngcinvALTV  40048  ringcinv  40087  ringcinvALTV  40111  srhmsubc  40131  srhmsubcALTV  40150  nnolog2flm1  40454