Theorem biimpcd 248

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimpac  478  axc16i  2436  nelneq  2863  nelneq2  2864  nssne1  3977  nssne2  3978  psssstr  4037  prproe  4834  iununi  5024  disjiun  5057  nbrne1  5089  nbrne2  5090  propeqop  5415  mosubopt  5418  relsnb  5701  relcnvtrg  6159  reuop  6185  dfpo2  6188  tz7.7  6277  suctr  6334  tz6.12i  6782  ssimaex  6835  chfnrn  6908  fvn0ssdmfun  6934  ffnfv  6974  f1elima  7117  elovmpt3rab1  7507  limsssuc  7672  nnsuc  7705  peano5  7714  peano5OLD  7715  dftpos4  8032  odi  8372  pssnn  8913  fineqvlem  8966  pssnnOLD  8969  ordunifi  8994  wdom2d  9269  r1pwss  9473  alephval3  9797  infdif  9896  cff1  9945  cofsmo  9956  axdc3lem2  10138  zorn2lem6  10188  cfpwsdom  10271  prub  10681  prnmadd  10684  1re  10906  letr  10999  dedekindle  11069  addid1  11085  negf1o  11335  negfi  11854  xrletr  12821  0fz1  13205  elfzmlbp  13296  leisorel  14102  elss2prb  14129  exprelprel  14131  fi1uzind  14139  swrdnd  14295  sqrmo  14891  isprm2  16315  nprmdvds1  16339  oddprmdvds  16532  catsubcat  17470  funcestrcsetclem8  17780  funcestrcsetclem9  17781  fthestrcsetc  17783  fullestrcsetc  17784  funcsetcestrclem9  17796  fthsetcestrc  17798  fullsetcestrc  17799  pltletr  17976  issstrmgm  18252  mgm2nsgrplem3  18474  sgrp2nmndlem3  18479  fvcosymgeq  18952  sylow2alem2  19138  islss  20111  gzrngunitlem  20575  pjdm2  20828  assamulgscmlem2  21014  gsumply1subr  21315  dmatmul  21554  decpmatmullem  21828  monmat2matmon  21881  chpscmat  21899  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  isclo2  22147  fbasfip  22927  ufileu  22978  alexsubALTlem2  23107  cnextcn  23126  metustbl  23628  elntg2  27256  ushgredgedg  27499  ushgredgedgloop  27501  edgnbusgreu  27637  nb3grprlem1  27650  cusgrfilem1  27725  cusgrfilem2  27726  umgr2v2evtxel  27792  wlkcompim  27901  usgr2pth  28033  usgr2trlncrct  28072  wwlknp  28109  wlkiswwlks2lem3  28137  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wwlksnext  28159  2pthdlem1  28196  umgr2adedgwlkonALT  28213  umgr2wlkon  28216  elwspths2spth  28233  rusgr0edg  28239  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a  28263  clwwisshclwwslem  28279  loopclwwlkn1b  28307  clwwlkel  28311  clwwlkext2edg  28321  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknonwwlknonb  28371  uhgr3cyclexlem  28446  upgr4cycl4dv4e  28450  eupth2lem3lem4  28496  frgruhgr0v  28529  numclwwlk1lem2f1  28622  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  frgrogt3nreg  28662  5oalem6  29922  eigorthi  30100  adjbd1o  30348  dmdbr7ati  30687  fmla1  33249  satffunlem2lem2  33268  fundmpss  33646  funbreq  33650  scutbdaybnd2lim  33938  idinside  34313  bj-opelidres  35259  bj-eldiag2  35275  bj-fvimacnv0  35384  poimirlem32  35736  sdclem2  35827  fdc1  35831  ismgmOLD  35935  lsatcvatlem  36990  atnle  37258  cvratlem  37362  ispsubcl2N  37888  trlord  38510  diaelrnN  38986  cdlemm10N  39059  dochexmidlem7  39407  fsuppind  40202  3impexpbicom  41988  sbcim2g  42047  suctrALT2VD  42345  suctrALT2  42346  3impexpVD  42365  3impexpbicomVD  42366  sbcim2gVD  42384  csbeq2gVD  42401  csbsngVD  42402  ax6e2ndeqVD  42418  2sb5ndVD  42419  infxrunb3rnmpt  42858  lptioo2  43062  lptioo1  43063  funressnfv  44424  ffnafv  44550  tz6.12i-afv2  44622  iccpartiltu  44762  iccpartigtl  44763  icceuelpartlem  44775  fargshiftfo  44782  ichnreuop  44812  reupr  44862  bgoldbtbndlem2  45146  mgmpropd  45217  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  srhmsubc  45522  srhmsubcALTV  45540  nnolog2flm1  45824  prelrrx2b  45948  rrxlinec  45970  eenglngeehlnm  45973