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  2441  nelneq  2859  nelneq2  2860  r19.35  3096  nssne1  4026  nssne2  4027  psssstr  4089  prproe  4886  iununi  5080  disjiun  5112  nbrne1  5143  nbrne2  5144  propeqop  5487  mosubopt  5490  relsnb  5786  relcnvtrg  6260  reuop  6287  dfpo2  6290  tz7.7  6383  suctr  6445  tz6.12i  6909  ssimaex  6969  chfnrn  7044  fvn0ssdmfun  7069  ffnfv  7114  f1elima  7261  elovmpt3rab1  7672  limsssuc  7850  nnsuc  7884  peano5  7894  dftpos4  8249  odi  8596  pssnn  9187  fineqvlem  9275  ordunifi  9303  wdom2d  9599  r1pwss  9803  alephval3  10129  infdif  10227  cff1  10277  cofsmo  10288  axdc3lem2  10470  zorn2lem6  10520  cfpwsdom  10603  prub  11013  prnmadd  11016  1re  11240  letr  11334  dedekindle  11404  addrid  11420  negf1o  11672  negfi  12196  xrletr  13179  0fz1  13566  elfzmlbp  13661  leisorel  14483  elss2prb  14511  exprelprel  14513  fi1uzind  14530  swrdnd  14677  sqrmo  15275  isprm2  16706  nprmdvds1  16730  oddprmdvds  16928  catsubcat  17857  funcestrcsetclem8  18164  funcestrcsetclem9  18165  fthestrcsetc  18167  fullestrcsetc  18168  funcsetcestrclem9  18180  fthsetcestrc  18182  fullsetcestrc  18183  pltletr  18358  mgmpropd  18634  issstrmgm  18636  mgm2nsgrplem3  18903  sgrp2nmndlem3  18908  fvcosymgeq  19415  sylow2alem2  19604  rngcinv  20602  srhmsubc  20645  islss  20896  gzrngunitlem  21405  pjdm2  21676  assamulgscmlem2  21865  gsumply1subr  22174  dmatmul  22440  decpmatmullem  22714  monmat2matmon  22767  chpscmat  22785  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  isclo2  23031  fbasfip  23811  ufileu  23862  alexsubALTlem2  23991  cnextcn  24010  metustbl  24510  scutbdaybnd2lim  27786  addsprop  27940  elntg2  28969  ushgredgedg  29213  ushgredgedgloop  29215  edgnbusgreu  29351  nb3grprlem1  29364  cusgrfilem1  29440  cusgrfilem2  29441  umgr2v2evtxel  29507  wlkcompim  29617  usgr2pth  29751  usgr2trlncrct  29793  wwlknp  29830  wlkiswwlks2lem3  29858  wlkiswwlksupgr2  29864  wlklnwwlkln2lem  29869  wwlksnext  29880  2pthdlem1  29917  umgr2adedgwlkonALT  29934  umgr2wlkon  29937  elwspths2spth  29954  rusgr0edg  29960  clwlkclwwlklem2a1  29978  clwlkclwwlklem2a  29984  clwwisshclwwslem  30000  loopclwwlkn1b  30028  clwwlkel  30032  clwwlkext2edg  30042  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  clwwlknonwwlknonb  30092  uhgr3cyclexlem  30167  upgr4cycl4dv4e  30171  eupth2lem3lem4  30217  frgruhgr0v  30250  numclwwlk1lem2f1  30343  numclwlk2lem2f  30363  numclwlk2lem2f1o  30365  frgrogt3nreg  30383  5oalem6  31645  eigorthi  31823  adjbd1o  32071  dmdbr7ati  32410  ssdifidlprm  33478  fmla1  35414  satffunlem2lem2  35433  fundmpss  35789  funbreq  35792  idinside  36107  bj-opelidres  37184  bj-eldiag2  37200  bj-fvimacnv0  37309  poimirlem32  37681  sdclem2  37771  fdc1  37775  ismgmOLD  37879  lsatcvatlem  39072  atnle  39340  cvratlem  39445  ispsubcl2N  39971  trlord  40593  diaelrnN  41069  cdlemm10N  41142  dochexmidlem7  41490  fsuppind  42588  3impexpbicom  44480  sbcim2g  44538  suctrALT2VD  44835  suctrALT2  44836  3impexpVD  44855  3impexpbicomVD  44856  sbcim2gVD  44874  csbeq2gVD  44891  csbsngVD  44892  ax6e2ndeqVD  44908  2sb5ndVD  44909  infxrunb3rnmpt  45435  lptioo2  45640  lptioo1  45641  funressnfv  47052  ffnafv  47180  tz6.12i-afv2  47252  iccpartiltu  47416  iccpartigtl  47417  icceuelpartlem  47429  fargshiftfo  47436  ichnreuop  47466  reupr  47516  bgoldbtbndlem2  47800  isubgredg  47859  upgrimtrlslem2  47898  cycl3grtrilem  47938  uspgrlimlem1  47980  rngcinvALTV  48231  srhmsubcALTV  48280  nnolog2flm1  48550  prelrrx2b  48674  rrxlinec  48696  eenglngeehlnm  48699