Theorem biimpcd 239

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

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

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 197

This theorem is referenced by:  biimpac  503  axc16i  2322  nelneq  2725  nelneq2  2726  nelne1  2890  nelne2  2891  nssne1  3661  nssne2  3662  psssstr  3713  prproe  4434  iununi  4610  disjiun  4640  nbrne1  4672  nbrne2  4673  propeqop  4970  mosubopt  4972  issref  5509  tz7.7  5749  suctr  5808  tz6.12i  6214  ssimaex  6263  chfnrn  6328  fvn0ssdmfun  6350  ffnfv  6388  f1elima  6520  elovmpt3rab1  6893  limsssuc  7050  nnsuc  7082  peano5  7089  dftpos4  7371  odi  7659  fineqvlem  8174  pssnn  8178  ordunifi  8210  wdom2d  8485  r1pwss  8647  alephval3  8933  infdif  9031  cff1  9080  cofsmo  9091  axdc3lem2  9273  zorn2lem6  9323  cfpwsdom  9406  prub  9816  prnmadd  9819  1re  10039  letr  10131  dedekindle  10201  addid1  10216  negf1o  10460  negfi  10971  xrletr  11989  0fz1  12361  elfzmlbp  12450  leisorel  13244  elss2prb  13269  exprelprel  13271  fi1uzind  13279  fi1uzindOLD  13285  swrdnd  13432  swrdccatfn  13482  sqrmo  13992  isprm2  15395  nprmdvds1  15418  oddprmdvds  15607  catsubcat  16499  funcestrcsetclem8  16787  funcestrcsetclem9  16788  fthestrcsetc  16790  fullestrcsetc  16791  funcsetcestrclem9  16803  fthsetcestrc  16805  fullsetcestrc  16806  pltletr  16971  issstrmgm  17252  mgm2nsgrplem3  17407  sgrp2nmndlem3  17412  fvcosymgeq  17849  sylow2alem2  18033  islss  18935  assamulgscmlem2  19349  gsumply1subr  19604  gzrngunitlem  19811  pjdm2  20055  dmatmul  20303  decpmatmullem  20576  monmat2matmon  20629  chpscmat  20647  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  isclo2  20892  fbasfip  21672  ufileu  21723  alexsubALTlem2  21852  cnextcn  21871  metustbl  22371  ushgredgedg  26121  ushgredgedgloop  26123  edgnbusgreu  26269  nb3grprlem1  26282  cusgrfilem1  26351  cusgrfilem2  26352  umgr2v2evtxel  26418  wlkcompim  26527  usgr2pth  26660  usgr2trlncrct  26698  wwlknp  26734  wlkiswwlks2lem3  26757  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wwlksnext  26788  2pthdlem1  26826  umgr2adedgwlkonALT  26843  umgr2wlkon  26846  elwspths2spth  26862  rusgr0edg  26868  isclwwlksnx  26889  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a  26899  clwwlksel  26914  clwwlksext2edg  26923  wwlksext2clwwlk  26924  clwwisshclwwslem  26927  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  clwlksf1clwwlklem2  26966  uhgr3cyclexlem  27041  upgr4cycl4dv4e  27045  eupth2lem3lem4  27091  frgruhgr0v  27127  numclwlk1lem2f1  27227  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  frgrogt3nreg  27255  5oalem6  28518  eigorthi  28696  adjbd1o  28944  dmdbr7ati  29283  dfpo2  31645  fundmpss  31664  funbreq  31668  idinside  32191  bj-eldiag2  33092  poimirlem32  33441  sdclem2  33538  fdc1  33542  ismgmOLD  33649  lsatcvatlem  34336  atnle  34604  cvratlem  34707  ispsubcl2N  35233  trlord  35857  diaelrnN  36334  cdlemm10N  36407  dochexmidlem7  36755  3impexpbicom  38685  sbcim2g  38748  suctrALT2VD  39071  suctrALT2  39072  3impexpVD  39091  3impexpbicomVD  39092  sbcim2gVD  39111  csbeq2gVD  39128  csbsngVD  39129  ax6e2ndeqVD  39145  2sb5ndVD  39146  infxrunb3rnmpt  39655  lptioo2  39863  lptioo1  39864  funressnfv  41208  ffnafv  41251  iccpartiltu  41358  iccpartigtl  41359  icceuelpartlem  41371  fargshiftfo  41378  bgoldbtbndlem2  41694  mgmpropd  41775  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  srhmsubc  42076  srhmsubcALTV  42094  nnolog2flm1  42384