Theorem biimpcd 249

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpac  478  axc16i  2436  nelneq  2855  nelneq2  2856  r19.35  3090  nssne1  3992  nssne2  3993  psssstr  4056  prproe  4854  iununi  5045  disjiun  5077  nbrne1  5108  nbrne2  5109  propeqop  5445  mosubopt  5448  relsnb  5741  relcnvtrg  6214  reuop  6240  dfpo2  6243  tz7.7  6332  suctr  6394  tz6.12i  6848  ssimaex  6907  chfnrn  6982  fvn0ssdmfun  7007  ffnfv  7052  f1elima  7197  elovmpt3rab1  7606  limsssuc  7780  nnsuc  7814  peano5  7823  dftpos4  8175  odi  8494  pssnn  9078  fineqvlem  9150  ordunifi  9174  wdom2d  9466  r1pwss  9677  alephval3  10001  infdif  10099  cff1  10149  cofsmo  10160  axdc3lem2  10342  zorn2lem6  10392  cfpwsdom  10475  prub  10885  prnmadd  10888  1re  11112  letr  11207  dedekindle  11277  addrid  11293  negf1o  11547  negfi  12071  xrletr  13057  0fz1  13444  elfzmlbp  13539  leisorel  14367  elss2prb  14395  exprelprel  14397  fi1uzind  14414  swrdnd  14562  sqrmo  15158  isprm2  16593  nprmdvds1  16617  oddprmdvds  16815  catsubcat  17746  funcestrcsetclem8  18053  funcestrcsetclem9  18054  fthestrcsetc  18056  fullestrcsetc  18057  funcsetcestrclem9  18069  fthsetcestrc  18071  fullsetcestrc  18072  pltletr  18247  mgmpropd  18559  issstrmgm  18561  mgm2nsgrplem3  18828  sgrp2nmndlem3  18833  fvcosymgeq  19341  sylow2alem2  19530  rngcinv  20552  srhmsubc  20595  islss  20867  gzrngunitlem  21369  pjdm2  21648  assamulgscmlem2  21837  gsumply1subr  22146  dmatmul  22412  decpmatmullem  22686  monmat2matmon  22739  chpscmat  22757  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  isclo2  23003  fbasfip  23783  ufileu  23834  alexsubALTlem2  23963  cnextcn  23982  metustbl  24481  scutbdaybnd2lim  27758  addsprop  27919  elntg2  28963  ushgredgedg  29207  ushgredgedgloop  29209  edgnbusgreu  29345  nb3grprlem1  29358  cusgrfilem1  29434  cusgrfilem2  29435  umgr2v2evtxel  29501  wlkcompim  29610  usgr2pth  29742  usgr2trlncrct  29784  wwlknp  29821  wlkiswwlks2lem3  29849  wlkiswwlksupgr2  29855  wlklnwwlkln2lem  29860  wwlksnext  29871  2pthdlem1  29908  umgr2adedgwlkonALT  29925  umgr2wlkon  29928  elwspths2spth  29948  rusgr0edg  29954  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a  29978  clwwisshclwwslem  29994  loopclwwlkn1b  30022  clwwlkel  30026  clwwlkext2edg  30036  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  clwwlknonwwlknonb  30086  uhgr3cyclexlem  30161  upgr4cycl4dv4e  30165  eupth2lem3lem4  30211  frgruhgr0v  30244  numclwwlk1lem2f1  30337  numclwlk2lem2f  30357  numclwlk2lem2f1o  30359  frgrogt3nreg  30377  5oalem6  31639  eigorthi  31817  adjbd1o  32065  dmdbr7ati  32404  ssdifidlprm  33423  fmla1  35431  satffunlem2lem2  35450  fundmpss  35811  funbreq  35814  idinside  36128  bj-opelidres  37205  bj-eldiag2  37221  bj-fvimacnv0  37330  poimirlem32  37702  sdclem2  37792  fdc1  37796  ismgmOLD  37900  lsatcvatlem  39158  atnle  39426  cvratlem  39530  ispsubcl2N  40056  trlord  40678  diaelrnN  41154  cdlemm10N  41227  dochexmidlem7  41575  fsuppind  42693  3impexpbicom  44583  sbcim2g  44641  suctrALT2VD  44938  suctrALT2  44939  3impexpVD  44958  3impexpbicomVD  44959  sbcim2gVD  44977  csbeq2gVD  44994  csbsngVD  44995  ax6e2ndeqVD  45011  2sb5ndVD  45012  infxrunb3rnmpt  45536  lptioo2  45741  lptioo1  45742  funressnfv  47153  ffnafv  47281  tz6.12i-afv2  47353  iccpartiltu  47532  iccpartigtl  47533  icceuelpartlem  47545  fargshiftfo  47552  ichnreuop  47582  reupr  47632  bgoldbtbndlem2  47916  isubgredg  47976  upgrimtrlslem2  48015  cycl3grtrilem  48056  uspgrlimlem1  48098  grlimprclnbgrvtx  48109  gpgedg2ov  48176  gpgedg2iv  48177  rngcinvALTV  48386  srhmsubcALTV  48435  nnolog2flm1  48701  prelrrx2b  48825  rrxlinec  48847  eenglngeehlnm  48850