Theorem biimpcd 238

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  biimpac  502  axc16i  2310  nelneq  2712  nelneq2  2713  nelne1  2878  nelne2  2879  nssne1  3624  nssne2  3625  psssstr  3675  iununi  4546  disjiun  4573  nbrne1  4602  nbrne2  4603  propeqop  4895  mosubopt  4897  issref  5428  tz7.7  5666  suctr  5725  tz6.12i  6124  ssimaex  6173  chfnrn  6236  fvn0ssdmfun  6258  ffnfv  6295  f1elima  6421  elovmpt3rab1  6791  limsssuc  6942  nnsuc  6974  peano5  6981  dftpos4  7258  odi  7546  fineqvlem  8059  pssnn  8063  ordunifi  8095  wdom2d  8368  r1pwss  8530  alephval3  8816  infdif  8914  cff1  8963  cofsmo  8974  axdc3lem2  9156  zorn2lem6  9206  cfpwsdom  9285  prub  9695  prnmadd  9698  1re  9918  letr  10010  dedekindle  10080  addid1  10095  negf1o  10339  negfi  10850  xrletr  11865  0fz1  12232  elfzmlbp  12319  leisorel  13101  elss2prb  13123  exprelprel  13126  fi1uzind  13134  fi1uzindOLD  13140  swrdnd  13284  swrdccatfn  13333  sqrmo  13840  isprm2  15233  nprmdvds1  15256  oddprmdvds  15445  catsubcat  16322  funcestrcsetclem8  16610  funcestrcsetclem9  16611  fthestrcsetc  16613  fullestrcsetc  16614  funcsetcestrclem9  16626  fthsetcestrc  16628  fullsetcestrc  16629  pltletr  16794  issstrmgm  17075  mgm2nsgrplem3  17230  sgrp2nmndlem3  17235  fvcosymgeq  17672  sylow2alem2  17856  islss  18756  assamulgscmlem2  19170  gsumply1subr  19425  gzrngunitlem  19630  pjdm2  19874  dmatmul  20122  decpmatmullem  20395  monmat2matmon  20448  chpscmat  20466  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  isclo2  20702  fbasfip  21482  ufileu  21533  alexsubALTlem2  21662  cnextcn  21681  metustbl  22181  usgrarnedg1  25918  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3graprlem1  25980  cusgrafilem2  26008  wlkn0  26055  fargshiftfo  26166  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  wlkiswwlk2lem3  26221  wlklniswwlkn1  26227  wlklniswwlkn2  26228  wwlknext  26252  clwwlknimp  26304  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a  26313  clwwlkel  26321  clwwlkext2edg  26330  wwlkext2clwwlk  26331  clwwisshclwwlem  26334  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfclwwlk  26371  clwlkf1clwwlklem2  26374  el2wlkonot  26396  el2wlkonotot1  26401  frgrancvvdeqlemA  26564  frgrancvvdeqlemC  26566  frgraeu  26581  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  frgraogt3nreg  26647  5oalem6  27902  eigorthi  28080  adjbd1o  28328  dmdbr7ati  28667  dfpo2  30898  fundmpss  30910  funbreq  30914  idinside  31361  bj-eldiag2  32269  poimirlem32  32611  sdclem2  32708  fdc1  32712  ismgmOLD  32819  lsatcvatlem  33354  atnle  33622  cvratlem  33725  ispsubcl2N  34251  trlord  34875  diaelrnN  35352  cdlemm10N  35425  dochexmidlem7  35773  3impexpbicom  37706  sbcim2g  37769  suctrALT2VD  38093  suctrALT2  38094  3impexpVD  38113  3impexpbicomVD  38114  sbcim2gVD  38133  csbeq2gVD  38150  csbsngVD  38151  ax6e2ndeqVD  38167  2sb5ndVD  38168  lptioo2  38698  lptioo1  38699  funressnfv  39857  ffnafv  39900  iccpartiltu  39960  iccpartigtl  39961  icceuelpartlem  39973  bgoldbtbndlem2  40222  ushgredgedga  40456  ushgredgedgaloop  40458  edgnbusgreu  40595  nb3grprlem1  40608  cusgrfilem1  40671  cusgrfilem2  40672  umgr2v2evtxel  40738  1wlkcompim  40836  usgr2trlncrct  41009  wwlknp  41045  1wlkiswwlks2lem3  41068  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  wwlksnext  41099  2pthdlem1  41137  umgr2adedgwlkonALT  41154  umgr2wlkon  41157  elwspths2spth  41171  rusgr0edg  41176  isclwwlksnx  41197  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a  41207  clwwlksel  41221  clwwlksext2edg  41230  wwlksext2clwwlk  41231  clwwisshclwwslem  41234  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  clwlksf1clwwlklem2  41273  uhgr3cyclexlem  41348  upgr4cycl4dv4e  41352  eupth2lem3lem4  41399  frgruhgr0v  41435  frgreu  41491  fusgr2wsp2nb  41498  av-numclwlk1lem2f1  41524  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-frgraogt3nreg  41551  mgmpropd  41565  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  srhmsubc  41868  srhmsubcALTV  41887  nnolog2flm1  42182  ssdifsn  42228