Theorem biimpcd 251

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimpac  481  axc16i  2454  nelneq  2937  nelneq2  2938  nelne1OLD  3114  nelne2OLD  3116  nssne1  4027  nssne2  4028  psssstr  4083  prproe  4830  iununi  5014  disjiun  5046  nbrne1  5078  nbrne2  5079  propeqop  5390  mosubopt  5393  relsnb  5670  relcnvtrg  6114  reuop  6139  tz7.7  6212  suctr  6269  tz6.12i  6691  ssimaex  6743  chfnrn  6814  fvn0ssdmfun  6837  ffnfv  6877  f1elima  7015  elovmpt3rab1  7399  limsssuc  7559  nnsuc  7591  peano5  7599  dftpos4  7905  odi  8199  fineqvlem  8726  pssnn  8730  ordunifi  8762  wdom2d  9038  r1pwss  9207  alephval3  9530  infdif  9625  cff1  9674  cofsmo  9685  axdc3lem2  9867  zorn2lem6  9917  cfpwsdom  10000  prub  10410  prnmadd  10413  1re  10635  letr  10728  dedekindle  10798  addid1  10814  negf1o  11064  negfi  11583  xrletr  12545  0fz1  12921  elfzmlbp  13012  leisorel  13812  elss2prb  13839  exprelprel  13841  fi1uzind  13849  swrdnd  14010  sqrmo  14605  isprm2  16020  nprmdvds1  16044  oddprmdvds  16233  catsubcat  17103  funcestrcsetclem8  17391  funcestrcsetclem9  17392  fthestrcsetc  17394  fullestrcsetc  17395  funcsetcestrclem9  17407  fthsetcestrc  17409  fullsetcestrc  17410  pltletr  17575  issstrmgm  17857  mgm2nsgrplem3  18079  sgrp2nmndlem3  18084  fvcosymgeq  18551  sylow2alem2  18737  islss  19700  assamulgscmlem2  20123  gsumply1subr  20396  gzrngunitlem  20604  pjdm2  20849  dmatmul  21100  decpmatmullem  21373  monmat2matmon  21426  chpscmat  21444  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  isclo2  21690  fbasfip  22470  ufileu  22521  alexsubALTlem2  22650  cnextcn  22669  metustbl  23170  elntg2  26765  ushgredgedg  27005  ushgredgedgloop  27007  edgnbusgreu  27143  nb3grprlem1  27156  cusgrfilem1  27231  cusgrfilem2  27232  umgr2v2evtxel  27298  wlkcompim  27407  usgr2pth  27539  usgr2trlncrct  27578  wwlknp  27615  wlkiswwlks2lem3  27643  wlkiswwlksupgr2  27649  wlklnwwlkln2lem  27654  wwlksnext  27665  2pthdlem1  27703  umgr2adedgwlkonALT  27720  umgr2wlkon  27723  elwspths2spth  27740  rusgr0edg  27746  clwlkclwwlklem2a1  27764  clwlkclwwlklem2a  27770  clwwisshclwwslem  27786  loopclwwlkn1b  27814  clwwlkel  27819  clwwlkext2edg  27829  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  clwwlknonwwlknonb  27879  uhgr3cyclexlem  27954  upgr4cycl4dv4e  27958  eupth2lem3lem4  28004  frgruhgr0v  28037  numclwwlk1lem2f1  28130  numclwlk2lem2f  28150  numclwlk2lem2f1o  28152  frgrogt3nreg  28170  5oalem6  29430  eigorthi  29608  adjbd1o  29856  dmdbr7ati  30195  fmla1  32629  satffunlem2lem2  32648  dfpo2  32986  fundmpss  33004  funbreq  33008  idinside  33540  bj-opelidres  34447  bj-eldiag2  34463  bj-imdirid  34469  bj-fvimacnv0  34562  poimirlem32  34918  sdclem2  35011  fdc1  35015  ismgmOLD  35122  lsatcvatlem  36179  atnle  36447  cvratlem  36551  ispsubcl2N  37077  trlord  37699  diaelrnN  38175  cdlemm10N  38248  dochexmidlem7  38596  3impexpbicom  40806  sbcim2g  40865  suctrALT2VD  41163  suctrALT2  41164  3impexpVD  41183  3impexpbicomVD  41184  sbcim2gVD  41202  csbeq2gVD  41219  csbsngVD  41220  ax6e2ndeqVD  41236  2sb5ndVD  41237  infxrunb3rnmpt  41694  lptioo2  41904  lptioo1  41905  funressnfv  43271  ffnafv  43363  tz6.12i-afv2  43435  iccpartiltu  43575  iccpartigtl  43576  icceuelpartlem  43588  fargshiftfo  43595  ichnreuop  43627  reupr  43677  bgoldbtbndlem2  43964  mgmpropd  44035  rngcinv  44245  rngcinvALTV  44257  ringcinv  44296  ringcinvALTV  44320  srhmsubc  44340  srhmsubcALTV  44358  nnolog2flm1  44643  prelrrx2b  44694  rrxlinec  44716  eenglngeehlnm  44719