Theorem biimpcd 249

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	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 245	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpac  478  axc16i  2434  nelneq  2852  nelneq2  2853  r19.35  3088  nssne1  4009  nssne2  4010  psssstr  4072  prproe  4869  iununi  5063  disjiun  5095  nbrne1  5126  nbrne2  5127  propeqop  5467  mosubopt  5470  relsnb  5765  relcnvtrg  6239  reuop  6266  dfpo2  6269  tz7.7  6358  suctr  6420  tz6.12i  6886  ssimaex  6946  chfnrn  7021  fvn0ssdmfun  7046  ffnfv  7091  f1elima  7238  elovmpt3rab1  7649  limsssuc  7826  nnsuc  7860  peano5  7869  dftpos4  8224  odi  8543  pssnn  9132  fineqvlem  9209  ordunifi  9237  wdom2d  9533  r1pwss  9737  alephval3  10063  infdif  10161  cff1  10211  cofsmo  10222  axdc3lem2  10404  zorn2lem6  10454  cfpwsdom  10537  prub  10947  prnmadd  10950  1re  11174  letr  11268  dedekindle  11338  addrid  11354  negf1o  11608  negfi  12132  xrletr  13118  0fz1  13505  elfzmlbp  13600  leisorel  14425  elss2prb  14453  exprelprel  14455  fi1uzind  14472  swrdnd  14619  sqrmo  15217  isprm2  16652  nprmdvds1  16676  oddprmdvds  16874  catsubcat  17801  funcestrcsetclem8  18108  funcestrcsetclem9  18109  fthestrcsetc  18111  fullestrcsetc  18112  funcsetcestrclem9  18124  fthsetcestrc  18126  fullsetcestrc  18127  pltletr  18302  mgmpropd  18578  issstrmgm  18580  mgm2nsgrplem3  18847  sgrp2nmndlem3  18852  fvcosymgeq  19359  sylow2alem2  19548  rngcinv  20546  srhmsubc  20589  islss  20840  gzrngunitlem  21349  pjdm2  21620  assamulgscmlem2  21809  gsumply1subr  22118  dmatmul  22384  decpmatmullem  22658  monmat2matmon  22711  chpscmat  22729  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  isclo2  22975  fbasfip  23755  ufileu  23806  alexsubALTlem2  23935  cnextcn  23954  metustbl  24454  scutbdaybnd2lim  27729  addsprop  27883  elntg2  28912  ushgredgedg  29156  ushgredgedgloop  29158  edgnbusgreu  29294  nb3grprlem1  29307  cusgrfilem1  29383  cusgrfilem2  29384  umgr2v2evtxel  29450  wlkcompim  29560  usgr2pth  29694  usgr2trlncrct  29736  wwlknp  29773  wlkiswwlks2lem3  29801  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wwlksnext  29823  2pthdlem1  29860  umgr2adedgwlkonALT  29877  umgr2wlkon  29880  elwspths2spth  29897  rusgr0edg  29903  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a  29927  clwwisshclwwslem  29943  loopclwwlkn1b  29971  clwwlkel  29975  clwwlkext2edg  29985  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknonwwlknonb  30035  uhgr3cyclexlem  30110  upgr4cycl4dv4e  30114  eupth2lem3lem4  30160  frgruhgr0v  30193  numclwwlk1lem2f1  30286  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  frgrogt3nreg  30326  5oalem6  31588  eigorthi  31766  adjbd1o  32014  dmdbr7ati  32353  ssdifidlprm  33429  fmla1  35374  satffunlem2lem2  35393  fundmpss  35754  funbreq  35757  idinside  36072  bj-opelidres  37149  bj-eldiag2  37165  bj-fvimacnv0  37274  poimirlem32  37646  sdclem2  37736  fdc1  37740  ismgmOLD  37844  lsatcvatlem  39042  atnle  39310  cvratlem  39415  ispsubcl2N  39941  trlord  40563  diaelrnN  41039  cdlemm10N  41112  dochexmidlem7  41460  fsuppind  42578  3impexpbicom  44470  sbcim2g  44528  suctrALT2VD  44825  suctrALT2  44826  3impexpVD  44845  3impexpbicomVD  44846  sbcim2gVD  44864  csbeq2gVD  44881  csbsngVD  44882  ax6e2ndeqVD  44898  2sb5ndVD  44899  infxrunb3rnmpt  45424  lptioo2  45629  lptioo1  45630  funressnfv  47044  ffnafv  47172  tz6.12i-afv2  47244  iccpartiltu  47423  iccpartigtl  47424  icceuelpartlem  47436  fargshiftfo  47443  ichnreuop  47473  reupr  47523  bgoldbtbndlem2  47807  isubgredg  47866  upgrimtrlslem2  47905  cycl3grtrilem  47945  uspgrlimlem1  47987  gpgedg2ov  48057  gpgedg2iv  48058  rngcinvALTV  48264  srhmsubcALTV  48313  nnolog2flm1  48579  prelrrx2b  48703  rrxlinec  48725  eenglngeehlnm  48728