Theorem biimpcd 252

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimpac  482  axc16i  2447  nelneq  2914  nelneq2  2915  nssne1  3975  nssne2  3976  psssstr  4034  prproe  4798  iununi  4984  disjiun  5017  nbrne1  5049  nbrne2  5050  propeqop  5362  mosubopt  5365  relsnb  5639  relcnvtrg  6086  reuop  6112  tz7.7  6185  suctr  6242  tz6.12i  6671  ssimaex  6723  chfnrn  6796  fvn0ssdmfun  6819  ffnfv  6859  f1elima  6999  elovmpt3rab1  7385  limsssuc  7545  nnsuc  7577  peano5  7585  dftpos4  7894  odi  8188  fineqvlem  8716  pssnn  8720  ordunifi  8752  wdom2d  9028  r1pwss  9197  alephval3  9521  infdif  9620  cff1  9669  cofsmo  9680  axdc3lem2  9862  zorn2lem6  9912  cfpwsdom  9995  prub  10405  prnmadd  10408  1re  10630  letr  10723  dedekindle  10793  addid1  10809  negf1o  11059  negfi  11577  xrletr  12539  0fz1  12922  elfzmlbp  13013  leisorel  13814  elss2prb  13841  exprelprel  13843  fi1uzind  13851  swrdnd  14007  sqrmo  14603  isprm2  16016  nprmdvds1  16040  oddprmdvds  16229  catsubcat  17101  funcestrcsetclem8  17389  funcestrcsetclem9  17390  fthestrcsetc  17392  fullestrcsetc  17393  funcsetcestrclem9  17405  fthsetcestrc  17407  fullsetcestrc  17408  pltletr  17573  issstrmgm  17855  mgm2nsgrplem3  18077  sgrp2nmndlem3  18082  fvcosymgeq  18549  sylow2alem2  18735  islss  19699  gzrngunitlem  20156  pjdm2  20400  assamulgscmlem2  20586  gsumply1subr  20863  dmatmul  21102  decpmatmullem  21376  monmat2matmon  21429  chpscmat  21447  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  isclo2  21693  fbasfip  22473  ufileu  22524  alexsubALTlem2  22653  cnextcn  22672  metustbl  23173  elntg2  26779  ushgredgedg  27019  ushgredgedgloop  27021  edgnbusgreu  27157  nb3grprlem1  27170  cusgrfilem1  27245  cusgrfilem2  27246  umgr2v2evtxel  27312  wlkcompim  27421  usgr2pth  27553  usgr2trlncrct  27592  wwlknp  27629  wlkiswwlks2lem3  27657  wlkiswwlksupgr2  27663  wlklnwwlkln2lem  27668  wwlksnext  27679  2pthdlem1  27716  umgr2adedgwlkonALT  27733  umgr2wlkon  27736  elwspths2spth  27753  rusgr0edg  27759  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a  27783  clwwisshclwwslem  27799  loopclwwlkn1b  27827  clwwlkel  27831  clwwlkext2edg  27841  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknonwwlknonb  27891  uhgr3cyclexlem  27966  upgr4cycl4dv4e  27970  eupth2lem3lem4  28016  frgruhgr0v  28049  numclwwlk1lem2f1  28142  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  frgrogt3nreg  28182  5oalem6  29442  eigorthi  29620  adjbd1o  29868  dmdbr7ati  30207  fmla1  32747  satffunlem2lem2  32766  dfpo2  33104  fundmpss  33122  funbreq  33126  idinside  33658  bj-opelidres  34576  bj-eldiag2  34592  bj-fvimacnv0  34701  poimirlem32  35089  sdclem2  35180  fdc1  35184  ismgmOLD  35288  lsatcvatlem  36345  atnle  36613  cvratlem  36717  ispsubcl2N  37243  trlord  37865  diaelrnN  38341  cdlemm10N  38414  dochexmidlem7  38762  fsuppind  39456  3impexpbicom  41185  sbcim2g  41244  suctrALT2VD  41542  suctrALT2  41543  3impexpVD  41562  3impexpbicomVD  41563  sbcim2gVD  41581  csbeq2gVD  41598  csbsngVD  41599  ax6e2ndeqVD  41615  2sb5ndVD  41616  infxrunb3rnmpt  42065  lptioo2  42273  lptioo1  42274  funressnfv  43635  ffnafv  43727  tz6.12i-afv2  43799  iccpartiltu  43939  iccpartigtl  43940  icceuelpartlem  43952  fargshiftfo  43959  ichnreuop  43989  reupr  44039  bgoldbtbndlem2  44324  mgmpropd  44395  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  srhmsubc  44700  srhmsubcALTV  44718  nnolog2flm1  45004  prelrrx2b  45128  rrxlinec  45150  eenglngeehlnm  45153