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  3971  nssne2  3972  psssstr  4036  prproe  4832  iununi  5058  disjiun  5090  nbrne1  5123  nbrne2  5124  propeqop  5479  mosubopt  5482  mosubott  5484  relsnb  5781  relcnvtrgOLD  6272  reuop  6299  dfpo2  6302  tz7.7  6391  suctr  6454  tz6.12i  6916  ssimaex  6975  chfnrn  7053  fvn0ssdmfun  7079  ffnfv  7124  f1elima  7271  elovmpt3rab1  7685  limsssuc  7865  nnsuc  7899  peano5  7909  dftpos4  8270  odi  8595  pssnn  9192  fineqvlem  9265  ordunifi  9289  wdom2d  9581  r1pwss  9798  alephval3  10196  infdif  10293  cff1  10343  cofsmo  10354  axdc3lem2  10536  zorn2lem6  10586  cfpwsdom  10676  prub  11086  prnmadd  11089  1re  11315  letr  11411  dedekindle  11481  addrid  11497  negf1o  11753  negfi  12273  xrletr  13294  0fz1  13684  elfzmlbp  13780  leisorel  14612  elss2prb  14640  exprelprel  14642  fi1uzind  14659  swrdnd  14812  sqrmo  15427  isprm2  16866  nprmdvds1  16891  oddprmdvds  17090  catsubcat  18023  funcestrcsetclem8  18330  funcestrcsetclem9  18331  fthestrcsetc  18333  fullestrcsetc  18334  funcsetcestrclem9  18346  fthsetcestrc  18348  fullsetcestrc  18349  pltletr  18524  mgmpropd  18838  issstrmgm  18840  mgm2nsgrplem3  19128  sgrp2nmndlem3  19133  fvcosymgeq  19652  sylow2alem2  19841  rngcinv  20898  srhmsubc  20941  islss  21218  ssdifidlprm  21651  gzrngunitlem  21747  pjdm2  22026  assamulgscmlem2  22217  gsumply1subr  22560  dmatmul  22821  decpmatmullem  23098  monmat2matmon  23151  chpscmat  23169  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  isclo2  23415  fbasfip  24196  ufileu  24247  alexsubALTlem2  24376  cnextcn  24395  metustbl  24894  cutbdaybnd2lim  28192  addsprop  28371  elntg2  29572  ushgredgedg  29819  ushgredgedgloop  29821  edgnbusgreu  29957  nb3grprlem1  29970  cusgrfilem1  30045  cusgrfilem2  30046  umgr2v2evtxel  30112  wlkcompim  30221  usgr2pth  30359  usgr2trlncrct  30404  wwlknp  30441  wlkiswwlks2lem3  30469  wlkiswwlksupgr2  30475  wlklnwwlkln2lem  30480  wwlksnext  30491  2pthdlem1  30528  umgr2adedgwlkonALT  30545  umgr2wlkon  30548  elwspths2spth  30568  rusgr0edg  30574  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a  30598  clwwisshclwwslem  30614  loopclwwlkn1b  30642  clwwlkel  30646  clwwlkext2edg  30656  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  clwwlknonwwlknonb  30706  uhgr3cyclexlem  30791  upgr4cycl4dv4e  30795  eupth2lem3lem4  30841  frgruhgr0v  30874  numclwwlk1lem2f1  30967  numclwlk2lem2f  30987  numclwlk2lem2f1o  30989  frgrogt3nreg  31007  5oalem6  32270  eigorthi  32448  adjbd1o  32696  dmdbr7ati  33035  erscottd  35819  acwer1prc  35828  fmla1  36270  satffunlem2lem2  36289  fundmpss  36656  funbreq  36658  idinside  36973  tr0elw  37396  tr0el  37397  dfttc4  37442  bj-opelidres  38219  bj-eldiag2  38235  bj-fvimacnv0  38344  wl-eujustlem1  38657  poimirlem32  38707  sdclem2  38813  fdc1  38817  ismgmOLD  38921  lsatcvatlem  40243  atnle  40511  cvratlem  40615  ispsubcl2N  41141  trlord  41763  diaelrnN  42239  cdlemm10N  42312  dochexmidlem7  42660  fsuppind  43755  3impexpbicom  45599  sbcim2g  45657  suctrALT2VD  45954  suctrALT2  45955  3impexpVD  45974  3impexpbicomVD  45975  sbcim2gVD  45993  csbeq2gVD  46010  csbsngVD  46011  ax6e2ndeqVD  46027  2sb5ndVD  46028  dmstructnn  46062  dmstructfi  46063  infxrunb3rnmpt  46574  lptioo2  46779  lptioo1  46780  funressnfv  48249  ffnafv  48377  tz6.12i-afv2  48449  iccpartiltu  48640  iccpartigtl  48641  icceuelpartlem  48653  fargshiftfo  48660  ichnreuop  48690  reupr  48740  bgoldbtbndlem2  49040  isubgredg  49100  upgrimtrlslem2  49139  cycl3grtrilem  49180  uspgrlimlem1  49222  grlimprclnbgrvtx  49233  gpgedg2ov  49300  gpgedg2iv  49301  rngcinvALTV  49509  srhmsubcALTV  49558  nnolog2flm1  49838  rrxlinec  49985