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  482  axc16i  2467  nelneq  2886  nelneq2  2887  r19.35  3120  nssne1  3998  nssne2  3999  psssstr  4063  prproe  4863  iununi  5056  disjiun  5088  nbrne1  5119  nbrne2  5120  propeqop  5476  mosubopt  5479  relsnb  5775  relcnvtrg  6254  reuop  6280  dfpo2  6283  tz7.7  6372  suctr  6434  tz6.12i  6893  ssimaex  6952  chfnrn  7030  fvn0ssdmfun  7055  ffnfv  7100  f1elima  7247  elovmpt3rab1  7656  limsssuc  7830  nnsuc  7864  peano5  7874  dftpos4  8225  odi  8548  pssnn  9137  fineqvlem  9210  ordunifi  9234  wdom2d  9528  r1pwss  9742  alephval3  10066  infdif  10164  cff1  10215  cofsmo  10226  axdc3lem2  10408  zorn2lem6  10458  cfpwsdom  10542  prub  10952  prnmadd  10955  1re  11181  letr  11277  dedekindle  11347  addrid  11363  negf1o  11617  negfi  12141  xrletr  13160  0fz1  13549  elfzmlbp  13644  leisorel  14473  elss2prb  14501  exprelprel  14503  fi1uzind  14520  swrdnd  14668  sqrmo  15278  isprm2  16716  nprmdvds1  16741  oddprmdvds  16939  catsubcat  17872  funcestrcsetclem8  18179  funcestrcsetclem9  18180  fthestrcsetc  18182  fullestrcsetc  18183  funcsetcestrclem9  18195  fthsetcestrc  18197  fullsetcestrc  18198  pltletr  18373  mgmpropd  18685  issstrmgm  18687  mgm2nsgrplem3  18957  sgrp2nmndlem3  18962  fvcosymgeq  19469  sylow2alem2  19658  rngcinv  20687  srhmsubc  20730  islss  21001  gzrngunitlem  21484  pjdm2  21763  assamulgscmlem2  21952  gsumply1subr  22295  dmatmul  22557  decpmatmullem  22831  monmat2matmon  22884  chpscmat  22902  chfacfscmulgsum  22920  chfacfpmmulgsum  22924  isclo2  23148  fbasfip  23928  ufileu  23979  alexsubALTlem2  24108  cnextcn  24127  metustbl  24626  cutbdaybnd2lim  27890  addsprop  28069  elntg2  29186  ushgredgedg  29430  ushgredgedgloop  29432  edgnbusgreu  29568  nb3grprlem1  29581  cusgrfilem1  29656  cusgrfilem2  29657  umgr2v2evtxel  29723  wlkcompim  29832  usgr2pth  29964  usgr2trlncrct  30006  wwlknp  30043  wlkiswwlks2lem3  30071  wlkiswwlksupgr2  30077  wlklnwwlkln2lem  30082  wwlksnext  30093  2pthdlem1  30130  umgr2adedgwlkonALT  30147  umgr2wlkon  30150  elwspths2spth  30170  rusgr0edg  30176  clwlkclwwlklem2a1  30194  clwlkclwwlklem2a  30200  clwwisshclwwslem  30216  loopclwwlkn1b  30244  clwwlkel  30248  clwwlkext2edg  30258  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  clwwlknonwwlknonb  30308  uhgr3cyclexlem  30383  upgr4cycl4dv4e  30387  eupth2lem3lem4  30433  frgruhgr0v  30466  numclwwlk1lem2f1  30559  numclwlk2lem2f  30579  numclwlk2lem2f1o  30581  frgrogt3nreg  30599  5oalem6  31862  eigorthi  32040  adjbd1o  32288  dmdbr7ati  32627  ssdifidlprm  33645  fmla1  35737  satffunlem2lem2  35756  fundmpss  36117  funbreq  36120  idinside  36434  tr0elw  36844  tr0el  36845  dfttc4  36890  bj-opelidres  37653  bj-eldiag2  37669  bj-fvimacnv0  37778  wl-eujustlem1  38091  poimirlem32  38151  sdclem2  38241  fdc1  38245  ismgmOLD  38349  lsatcvatlem  39673  atnle  39941  cvratlem  40045  ispsubcl2N  40571  trlord  41193  diaelrnN  41669  cdlemm10N  41742  dochexmidlem7  42090  fsuppind  43172  3impexpbicom  45056  sbcim2g  45114  suctrALT2VD  45411  suctrALT2  45412  3impexpVD  45431  3impexpbicomVD  45432  sbcim2gVD  45450  csbeq2gVD  45467  csbsngVD  45468  ax6e2ndeqVD  45484  2sb5ndVD  45485  infxrunb3rnmpt  46002  lptioo2  46207  lptioo1  46208  funressnfv  47637  ffnafv  47765  tz6.12i-afv2  47837  iccpartiltu  48028  iccpartigtl  48029  icceuelpartlem  48041  fargshiftfo  48048  ichnreuop  48078  reupr  48128  bgoldbtbndlem2  48428  isubgredg  48488  upgrimtrlslem2  48527  cycl3grtrilem  48568  uspgrlimlem1  48610  grlimprclnbgrvtx  48621  gpgedg2ov  48688  gpgedg2iv  48689  rngcinvALTV  48898  srhmsubcALTV  48947  nnolog2flm1  49212  prelrrx2b  49336  rrxlinec  49358  eenglngeehlnm  49361