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 23	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 248	1 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpac  484  axc16i  2465  nelneq  2884  nelneq2  2885  r19.35  3120  nssne1  3993  nssne2  3994  psssstr  4058  prproe  4865  iununi  5059  disjiun  5091  nbrne1  5124  nbrne2  5125  propeqop  5484  mosubopt  5487  relsnb  5783  relcnvtrgOLD  6264  reuop  6291  dfpo2  6294  tz7.7  6383  suctr  6446  tz6.12i  6905  ssimaex  6964  chfnrn  7042  fvn0ssdmfun  7068  ffnfv  7113  f1elima  7261  elovmpt3rab1  7675  limsssuc  7847  nnsuc  7881  peano5  7891  dftpos4  8244  odi  8567  pssnn  9164  fineqvlem  9237  ordunifi  9261  wdom2d  9553  r1pwss  9767  alephval3  10114  infdif  10211  cff1  10261  cofsmo  10272  axdc3lem2  10454  zorn2lem6  10504  cfpwsdom  10594  prub  11004  prnmadd  11007  1re  11233  letr  11329  dedekindle  11399  addrid  11415  negf1o  11669  negfi  12189  xrletr  13210  0fz1  13599  elfzmlbp  13695  leisorel  14526  elss2prb  14554  exprelprel  14556  fi1uzind  14573  swrdnd  14725  sqrmo  15339  isprm2  16773  nprmdvds1  16798  oddprmdvds  16996  catsubcat  17929  funcestrcsetclem8  18236  funcestrcsetclem9  18237  fthestrcsetc  18239  fullestrcsetc  18240  funcsetcestrclem9  18252  fthsetcestrc  18254  fullsetcestrc  18255  pltletr  18430  mgmpropd  18744  issstrmgm  18746  mgm2nsgrplem3  19033  sgrp2nmndlem3  19038  fvcosymgeq  19557  sylow2alem2  19746  rngcinv  20800  srhmsubc  20843  islss  21119  ssdifidlprm  21550  gzrngunitlem  21646  pjdm2  21925  assamulgscmlem2  22116  gsumply1subr  22459  dmatmul  22720  decpmatmullem  22997  monmat2matmon  23050  chpscmat  23068  chfacfscmulgsum  23086  chfacfpmmulgsum  23090  isclo2  23314  fbasfip  24095  ufileu  24146  alexsubALTlem2  24275  cnextcn  24294  metustbl  24793  cutbdaybnd2lim  28063  addsprop  28242  elntg2  29443  ushgredgedg  29690  ushgredgedgloop  29692  edgnbusgreu  29828  nb3grprlem1  29841  cusgrfilem1  29916  cusgrfilem2  29917  umgr2v2evtxel  29983  wlkcompim  30092  usgr2pth  30230  usgr2trlncrct  30275  wwlknp  30312  wlkiswwlks2lem3  30340  wlkiswwlksupgr2  30346  wlklnwwlkln2lem  30351  wwlksnext  30362  2pthdlem1  30399  umgr2adedgwlkonALT  30416  umgr2wlkon  30419  elwspths2spth  30439  rusgr0edg  30445  clwlkclwwlklem2a1  30463  clwlkclwwlklem2a  30469  clwwisshclwwslem  30485  loopclwwlkn1b  30513  clwwlkel  30517  clwwlkext2edg  30527  hashecclwwlkn1  30548  umgrhashecclwwlk  30549  clwwlknonwwlknonb  30577  uhgr3cyclexlem  30662  upgr4cycl4dv4e  30666  eupth2lem3lem4  30712  frgruhgr0v  30745  numclwwlk1lem2f1  30838  numclwlk2lem2f  30858  numclwlk2lem2f1o  30860  frgrogt3nreg  30878  5oalem6  32141  eigorthi  32319  adjbd1o  32567  dmdbr7ati  32906  fmla1  35967  satffunlem2lem2  35986  fundmpss  36347  funbreq  36350  idinside  36665  tr0elw  37104  tr0el  37105  dfttc4  37150  bj-opelidres  37914  bj-eldiag2  37930  bj-fvimacnv0  38039  wl-eujustlem1  38352  poimirlem32  38402  sdclem2  38493  fdc1  38497  ismgmOLD  38601  lsatcvatlem  39923  atnle  40191  cvratlem  40295  ispsubcl2N  40821  trlord  41443  diaelrnN  41919  cdlemm10N  41992  dochexmidlem7  42340  fsuppind  43437  3impexpbicom  45304  sbcim2g  45362  suctrALT2VD  45659  suctrALT2  45660  3impexpVD  45679  3impexpbicomVD  45680  sbcim2gVD  45698  csbeq2gVD  45715  csbsngVD  45716  ax6e2ndeqVD  45732  2sb5ndVD  45733  infxrunb3rnmpt  46257  lptioo2  46462  lptioo1  46463  funressnfv  47932  ffnafv  48060  tz6.12i-afv2  48132  iccpartiltu  48323  iccpartigtl  48324  icceuelpartlem  48336  fargshiftfo  48343  ichnreuop  48373  reupr  48423  bgoldbtbndlem2  48723  isubgredg  48783  upgrimtrlslem2  48822  cycl3grtrilem  48863  uspgrlimlem1  48905  grlimprclnbgrvtx  48916  gpgedg2ov  48983  gpgedg2iv  48984  rngcinvALTV  49192  srhmsubcALTV  49241  nnolog2flm1  49521  prelrrx2b  49645  rrxlinec  49667  eenglngeehlnm  49670