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  2468  nelneq  2888  nelneq2  2889  r19.35  3124  nssne1  3975  nssne2  3976  psssstr  4040  prproe  4838  iununi  5064  disjiun  5096  nbrne1  5130  nbrne2  5131  propeqop  5486  mosubopt  5489  mosubott  5491  relsnb  5789  relcnvtrgOLD  6293  reuop  6322  dfpo2  6325  tz7.7  6414  suctr  6477  tz6.12i  6942  ssimaex  7001  chfnrn  7079  fvn0ssdmfun  7106  ffnfv  7151  f1elima  7298  elovmpt3rab1  7713  limsssuc  7895  nnsuc  7929  peano5  7939  dftpos4  8300  odi  8625  pssnn  9222  fineqvlem  9295  ordunifi  9319  wdom2d  9611  r1pwss  9828  alephval3  10228  infdif  10325  cff1  10375  cofsmo  10386  axdc3lem2  10568  zorn2lem6  10618  cfpwsdom  10708  prub  11118  prnmadd  11121  1re  11347  letr  11443  dedekindle  11513  addrid  11529  negf1o  11785  negfi  12306  xrletr  13327  0fz1  13717  elfzmlbp  13813  leisorel  14646  elss2prb  14674  exprelprel  14676  fi1uzind  14693  swrdnd  14846  sqrmo  15461  isprm2  16901  nprmdvds1  16926  oddprmdvds  17125  catsubcat  18064  funcestrcsetclem8  18371  funcestrcsetclem9  18372  fthestrcsetc  18374  fullestrcsetc  18375  funcsetcestrclem9  18387  fthsetcestrc  18389  fullsetcestrc  18390  pltletr  18565  mgmpropd  18879  issstrmgm  18881  mgm2nsgrplem3  19169  sgrp2nmndlem3  19174  fvcosymgeq  19694  sylow2alem2  19883  rngcinv  20940  srhmsubc  20983  islss  21260  ssdifidlprm  21693  gzrngunitlem  21792  pjdm2  22072  assamulgscmlem2  22263  gsumply1subr  22606  dmatmul  22867  decpmatmullem  23144  monmat2matmon  23197  chpscmat  23215  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  isclo2  23461  fbasfip  24242  ufileu  24293  alexsubALTlem2  24422  cnextcn  24441  metustbl  24940  cutbdaybnd2lim  28240  addsprop  28419  elntg2  29620  ushgredgedg  29867  ushgredgedgloop  29869  edgnbusgreu  30005  nb3grprlem1  30018  cusgrfilem1  30093  cusgrfilem2  30094  umgr2v2evtxel  30160  wlkcompim  30269  usgr2pth  30407  usgr2trlncrct  30452  wwlknp  30489  wlkiswwlks2lem3  30517  wlkiswwlksupgr2  30523  wlklnwwlkln2lem  30528  wwlksnext  30539  2pthdlem1  30576  umgr2adedgwlkonALT  30593  umgr2wlkon  30596  elwspths2spth  30616  rusgr0edg  30622  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a  30646  clwwisshclwwslem  30662  loopclwwlkn1b  30690  clwwlkel  30694  clwwlkext2edg  30704  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  clwwlknonwwlknonb  30754  uhgr3cyclexlem  30839  upgr4cycl4dv4e  30843  eupth2lem3lem4  30889  frgruhgr0v  30922  numclwwlk1lem2f1  31015  numclwlk2lem2f  31035  numclwlk2lem2f1o  31037  frgrogt3nreg  31055  5oalem6  32318  eigorthi  32496  adjbd1o  32744  dmdbr7ati  33083  erscottd  35884  acwer1prc  35893  fmla1  36360  satffunlem2lem2  36379  fundmpss  36747  funbreq  36749  idinside  37064  tr0elw  37487  tr0el  37488  dfttc4  37533  bj-opelidres  38350  bj-eldiag2  38366  bj-fvimacnv0  38475  wl-eujustlem1  38788  poimirlem32  38838  sdclem2  38942  fdc1  38946  ismgmOLD  39050  lsatcvatlem  40372  atnle  40640  cvratlem  40744  ispsubcl2N  41270  trlord  41892  diaelrnN  42368  cdlemm10N  42441  dochexmidlem7  42789  fsuppind  43884  3impexpbicom  45723  sbcim2g  45781  suctrALT2VD  46078  suctrALT2  46079  3impexpVD  46098  3impexpbicomVD  46099  sbcim2gVD  46117  csbeq2gVD  46134  csbsngVD  46135  ax6e2ndeqVD  46151  2sb5ndVD  46152  dmstructnn  46188  dmstructfi  46189  infxrunb3rnmpt  46711  lptioo2  46916  lptioo1  46917  funressnfv  48386  ffnafv  48514  tz6.12i-afv2  48586  iccpartiltu  48777  iccpartigtl  48778  icceuelpartlem  48790  fargshiftfo  48797  ichnreuop  48827  reupr  48877  bgoldbtbndlem2  49177  isubgredg  49237  upgrimtrlslem2  49276  cycl3grtrilem  49317  uspgrlimlem1  49359  grlimprclnbgrvtx  49370  gpgedg2ov  49437  gpgedg2iv  49438  rngcinvALTV  49646  srhmsubcALTV  49695  nnolog2flm1  50033  rrxlinec  50180