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  2458  nelneq  2937  nelneq2  2938  nelne1OLD  3114  nelne2OLD  3116  nssne1  4027  nssne2  4028  psssstr  4083  prproe  4836  iununi  5021  disjiun  5053  nbrne1  5085  nbrne2  5086  propeqop  5397  mosubopt  5400  relsnb  5675  relcnvtrg  6119  reuop  6144  tz7.7  6217  suctr  6274  tz6.12i  6696  ssimaex  6748  chfnrn  6819  fvn0ssdmfun  6842  ffnfv  6882  f1elima  7021  elovmpt3rab1  7405  limsssuc  7565  nnsuc  7597  peano5  7605  dftpos4  7911  odi  8205  fineqvlem  8732  pssnn  8736  ordunifi  8768  wdom2d  9044  r1pwss  9213  alephval3  9536  infdif  9631  cff1  9680  cofsmo  9691  axdc3lem2  9873  zorn2lem6  9923  cfpwsdom  10006  prub  10416  prnmadd  10419  1re  10641  letr  10734  dedekindle  10804  addid1  10820  negf1o  11070  negfi  11589  xrletr  12552  0fz1  12928  elfzmlbp  13019  leisorel  13819  elss2prb  13846  exprelprel  13848  fi1uzind  13856  swrdnd  14016  sqrmo  14611  isprm2  16026  nprmdvds1  16050  oddprmdvds  16239  catsubcat  17109  funcestrcsetclem8  17397  funcestrcsetclem9  17398  fthestrcsetc  17400  fullestrcsetc  17401  funcsetcestrclem9  17413  fthsetcestrc  17415  fullsetcestrc  17416  pltletr  17581  issstrmgm  17863  mgm2nsgrplem3  18085  sgrp2nmndlem3  18090  fvcosymgeq  18557  sylow2alem2  18743  islss  19706  assamulgscmlem2  20129  gsumply1subr  20402  gzrngunitlem  20610  pjdm2  20855  dmatmul  21106  decpmatmullem  21379  monmat2matmon  21432  chpscmat  21450  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  isclo2  21696  fbasfip  22476  ufileu  22527  alexsubALTlem2  22656  cnextcn  22675  metustbl  23176  elntg2  26771  ushgredgedg  27011  ushgredgedgloop  27013  edgnbusgreu  27149  nb3grprlem1  27162  cusgrfilem1  27237  cusgrfilem2  27238  umgr2v2evtxel  27304  wlkcompim  27413  usgr2pth  27545  usgr2trlncrct  27584  wwlknp  27621  wlkiswwlks2lem3  27649  wlkiswwlksupgr2  27655  wlklnwwlkln2lem  27660  wwlksnext  27671  2pthdlem1  27709  umgr2adedgwlkonALT  27726  umgr2wlkon  27729  elwspths2spth  27746  rusgr0edg  27752  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a  27776  clwwisshclwwslem  27792  loopclwwlkn1b  27820  clwwlkel  27825  clwwlkext2edg  27835  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknonwwlknonb  27885  uhgr3cyclexlem  27960  upgr4cycl4dv4e  27964  eupth2lem3lem4  28010  frgruhgr0v  28043  numclwwlk1lem2f1  28136  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  frgrogt3nreg  28176  5oalem6  29436  eigorthi  29614  adjbd1o  29862  dmdbr7ati  30201  fmla1  32634  satffunlem2lem2  32653  dfpo2  32991  fundmpss  33009  funbreq  33013  idinside  33545  bj-opelidres  34456  bj-eldiag2  34472  bj-imdirid  34478  bj-fvimacnv0  34571  poimirlem32  34939  sdclem2  35032  fdc1  35036  ismgmOLD  35143  lsatcvatlem  36200  atnle  36468  cvratlem  36572  ispsubcl2N  37098  trlord  37720  diaelrnN  38196  cdlemm10N  38269  dochexmidlem7  38617  3impexpbicom  40833  sbcim2g  40892  suctrALT2VD  41190  suctrALT2  41191  3impexpVD  41210  3impexpbicomVD  41211  sbcim2gVD  41229  csbeq2gVD  41246  csbsngVD  41247  ax6e2ndeqVD  41263  2sb5ndVD  41264  infxrunb3rnmpt  41722  lptioo2  41932  lptioo1  41933  funressnfv  43298  ffnafv  43390  tz6.12i-afv2  43462  iccpartiltu  43602  iccpartigtl  43603  icceuelpartlem  43615  fargshiftfo  43622  ichnreuop  43654  reupr  43704  bgoldbtbndlem2  43991  mgmpropd  44062  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  srhmsubc  44367  srhmsubcALTV  44385  nnolog2flm1  44670  prelrrx2b  44721  rrxlinec  44743  eenglngeehlnm  44746