Theorem biimpcd 232

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 228	1 |- ( ps -> ( ph -> ch ) )

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

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 190

This theorem is referenced by:  biimpac  494  axc16i  2171  nelneq  2573  nelneq2  2574  nelne1  2739  nelne2  2740  nssne1  3474  nssne2  3475  psssstr  3525  difsn  4097  iununi  4359  disjiun  4386  nbrne1  4413  nbrne2  4414  mosubopt  4699  issref  5219  tz7.7  5456  tz6.12i  5899  ssimaex  5945  chfnrn  6008  fvn0ssdmfun  6028  ffnfv  6064  f1elima  6182  elovmpt3rab1  6546  limsssuc  6696  nnsuc  6728  peano5  6735  dftpos4  7010  odi  7298  fineqvlem  7804  pssnn  7808  ordunifi  7839  wdom2d  8113  r1pwss  8273  alephval3  8559  infdif  8657  cff1  8706  cofsmo  8717  axdc3lem2  8899  zorn2lem6  8949  cfpwsdom  9027  prub  9437  prnmadd  9440  1re  9660  letr  9745  dedekindle  9816  addid1  9831  negf1o  10070  negfi  10576  xrletr  11478  0fz1  11845  elfzmlbp  11927  leisorel  12664  elss2prb  12684  exprelprel  12687  fi1uzind  12691  fi1uzindOLD  12697  swrdnd  12842  swrdccatfn  12892  sqrmo  13392  dvdseq  14429  isprm2  14711  nprmdvds1  14729  catsubcat  15822  funcestrcsetclem8  16110  funcestrcsetclem9  16111  fthestrcsetc  16113  fullestrcsetc  16114  funcsetcestrclem9  16126  fthsetcestrc  16128  fullsetcestrc  16129  pltletr  16295  mgm2nsgrplem3  16732  sgrp2nmndlem3  16737  fvcosymgeq  17148  sylow2alem2  17348  islss  18236  assamulgscmlem2  18650  gsumply1subr  18904  gzrngunitlem  19109  pjdm2  19351  dmatmul  19599  decpmatmullem  19872  monmat2matmon  19925  chpscmat  19943  chfacfscmulgsum  19961  chfacfpmmulgsum  19965  isclo2  20181  fbasfip  20961  ufileu  21012  alexsubALTlem2  21141  cnextcn  21160  metustbl  21659  usgrarnedg1  25195  nbgraf1olem3  25250  nbgraf1olem5  25252  nb3graprlem1  25258  cusgrafilem2  25287  wlkn0  25334  fargshiftfo  25445  3v3e3cycl1  25451  4cycl4v4e  25473  4cycl4dv4e  25475  wlkiswwlk2lem3  25500  wlklniswwlkn1  25506  wlklniswwlkn2  25507  wwlknext  25531  clwwlknimp  25583  clwlkisclwwlklem2a1  25586  clwlkisclwwlklem2a  25592  clwwlkel  25600  clwwlkext2edg  25609  wwlkext2clwwlk  25610  clwwisshclwwlem  25613  hashecclwwlkn1  25641  usghashecclwwlk  25642  clwlkfclwwlk  25651  clwlkf1clwwlklem2  25654  el2wlkonot  25676  el2wlkonotot1  25681  frgrancvvdeqlemA  25844  frgrancvvdeqlemC  25846  frgraeu  25861  numclwlk2lem2f  25910  numclwlk2lem2f1o  25912  frgraogt3nreg  25927  ismgmOLD  26129  5oalem6  27393  eigorthi  27571  adjbd1o  27819  dmdbr7ati  28158  dfpo2  30466  fundmpss  30478  funbreq  30482  idinside  30922  bj-eldiag2  31717  poimirlem32  32036  sdclem2  32135  fdc1  32139  lsatcvatlem  32686  atnle  32954  cvratlem  33057  ispsubcl2N  33583  trlord  34207  diaelrnN  34684  cdlemm10N  34757  dochexmidlem7  35105  3impexpbicom  36904  sbcim2g  36969  suctrALT2VD  37295  suctrALT2  37296  3impexpVD  37315  3impexpbicomVD  37316  sbcim2gVD  37335  csbeq2gVD  37352  csbsngVD  37353  ax6e2ndeqVD  37369  2sb5ndVD  37370  lptioo2  37808  lptioo1  37809  funressnfv  38774  ffnafv  38818  iccpartiltu  38881  iccpartigtl  38882  icceuelpartlem  38894  oddprmuzge3  38986  bgoldbtbndlem2  39046  propeqop  39146  ushgredgedga  39470  ushgredgedgaloop  39472  edgnbusgreu  39605  nb3grprlem1  39618  cusgrfilem1  39681  cusgrfilem2  39682  umgr2v2evtxel  39745  1wlkn0  39825  1wlkcompim  39834  2pthdlem1  40052  umgr2adedgwlkonALT  40069  umgr2wlkon  40072  uhgr3cyclexlem  40095  upgr4cycl4dv4e  40099  eupth2lem3lem4  40143  usgedgimp  40223  usgedgimpALT  40226  fusgraimpcl  40247  fusgraimpclALT  40249  fusgraimpclALT2  40251  mgmpropd  40283  rngcinv  40491  rngcinvALTV  40503  ringcinv  40542  ringcinvALTV  40566  srhmsubc  40586  srhmsubcALTV  40605  nnolog2flm1  40909