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  2436  nelneq  2857  nelneq2  2858  nssne1  3937  nssne2  3938  psssstr  3997  prproe  4794  iununi  4984  disjiun  5017  nbrne1  5049  nbrne2  5050  propeqop  5364  mosubopt  5367  relsnb  5646  relcnvtrg  6099  reuop  6125  tz7.7  6198  suctr  6255  tz6.12i  6700  ssimaex  6753  chfnrn  6826  fvn0ssdmfun  6852  ffnfv  6892  f1elima  7032  elovmpt3rab1  7421  limsssuc  7584  nnsuc  7616  peano5  7624  peano5OLD  7625  dftpos4  7940  odi  8236  pssnn  8767  fineqvlem  8811  pssnnOLD  8815  ordunifi  8842  wdom2d  9117  r1pwss  9286  alephval3  9610  infdif  9709  cff1  9758  cofsmo  9769  axdc3lem2  9951  zorn2lem6  10001  cfpwsdom  10084  prub  10494  prnmadd  10497  1re  10719  letr  10812  dedekindle  10882  addid1  10898  negf1o  11148  negfi  11667  xrletr  12634  0fz1  13018  elfzmlbp  13109  leisorel  13912  elss2prb  13939  exprelprel  13941  fi1uzind  13949  swrdnd  14105  sqrmo  14701  isprm2  16123  nprmdvds1  16147  oddprmdvds  16339  catsubcat  17214  funcestrcsetclem8  17513  funcestrcsetclem9  17514  fthestrcsetc  17516  fullestrcsetc  17517  funcsetcestrclem9  17529  fthsetcestrc  17531  fullsetcestrc  17532  pltletr  17697  issstrmgm  17979  mgm2nsgrplem3  18201  sgrp2nmndlem3  18206  fvcosymgeq  18675  sylow2alem2  18861  islss  19825  gzrngunitlem  20282  pjdm2  20527  assamulgscmlem2  20714  gsumply1subr  21009  dmatmul  21248  decpmatmullem  21522  monmat2matmon  21575  chpscmat  21593  chfacfscmulgsum  21611  chfacfpmmulgsum  21615  isclo2  21839  fbasfip  22619  ufileu  22670  alexsubALTlem2  22799  cnextcn  22818  metustbl  23319  elntg2  26931  ushgredgedg  27171  ushgredgedgloop  27173  edgnbusgreu  27309  nb3grprlem1  27322  cusgrfilem1  27397  cusgrfilem2  27398  umgr2v2evtxel  27464  wlkcompim  27573  usgr2pth  27705  usgr2trlncrct  27744  wwlknp  27781  wlkiswwlks2lem3  27809  wlkiswwlksupgr2  27815  wlklnwwlkln2lem  27820  wwlksnext  27831  2pthdlem1  27868  umgr2adedgwlkonALT  27885  umgr2wlkon  27888  elwspths2spth  27905  rusgr0edg  27911  clwlkclwwlklem2a1  27929  clwlkclwwlklem2a  27935  clwwisshclwwslem  27951  loopclwwlkn1b  27979  clwwlkel  27983  clwwlkext2edg  27993  hashecclwwlkn1  28014  umgrhashecclwwlk  28015  clwwlknonwwlknonb  28043  uhgr3cyclexlem  28118  upgr4cycl4dv4e  28122  eupth2lem3lem4  28168  frgruhgr0v  28201  numclwwlk1lem2f1  28294  numclwlk2lem2f  28314  numclwlk2lem2f1o  28316  frgrogt3nreg  28334  5oalem6  29594  eigorthi  29772  adjbd1o  30020  dmdbr7ati  30359  fmla1  32920  satffunlem2lem2  32939  dfpo2  33294  fundmpss  33312  funbreq  33316  scutbdaybnd2lim  33652  idinside  34024  bj-opelidres  34953  bj-eldiag2  34969  bj-fvimacnv0  35078  poimirlem32  35432  sdclem2  35523  fdc1  35527  ismgmOLD  35631  lsatcvatlem  36686  atnle  36954  cvratlem  37058  ispsubcl2N  37584  trlord  38206  diaelrnN  38682  cdlemm10N  38755  dochexmidlem7  39103  fsuppind  39858  3impexpbicom  41637  sbcim2g  41696  suctrALT2VD  41994  suctrALT2  41995  3impexpVD  42014  3impexpbicomVD  42015  sbcim2gVD  42033  csbeq2gVD  42050  csbsngVD  42051  ax6e2ndeqVD  42067  2sb5ndVD  42068  infxrunb3rnmpt  42506  lptioo2  42714  lptioo1  42715  funressnfv  44076  ffnafv  44196  tz6.12i-afv2  44268  iccpartiltu  44408  iccpartigtl  44409  icceuelpartlem  44421  fargshiftfo  44428  ichnreuop  44458  reupr  44508  bgoldbtbndlem2  44792  mgmpropd  44863  rngcinv  45073  rngcinvALTV  45085  ringcinv  45124  ringcinvALTV  45148  srhmsubc  45168  srhmsubcALTV  45186  nnolog2flm1  45470  prelrrx2b  45594  rrxlinec  45616  eenglngeehlnm  45619