Theorem biimpcd 248

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimpac  479  axc16i  2437  nelneq  2864  nelneq2  2865  nssne1  3982  nssne2  3983  psssstr  4042  prproe  4838  iununi  5029  disjiun  5062  nbrne1  5094  nbrne2  5095  propeqop  5422  mosubopt  5425  relsnb  5714  relcnvtrg  6174  reuop  6200  dfpo2  6203  tz7.7  6296  suctr  6353  tz6.12i  6809  ssimaex  6862  chfnrn  6935  fvn0ssdmfun  6961  ffnfv  7001  f1elima  7145  elovmpt3rab1  7538  limsssuc  7706  nnsuc  7739  peano5  7749  peano5OLD  7750  dftpos4  8070  odi  8419  pssnn  8960  fineqvlem  9046  pssnnOLD  9049  ordunifi  9073  wdom2d  9348  r1pwss  9551  alephval3  9875  infdif  9974  cff1  10023  cofsmo  10034  axdc3lem2  10216  zorn2lem6  10266  cfpwsdom  10349  prub  10759  prnmadd  10762  1re  10984  letr  11078  dedekindle  11148  addid1  11164  negf1o  11414  negfi  11933  xrletr  12901  0fz1  13285  elfzmlbp  13376  leisorel  14183  elss2prb  14210  exprelprel  14212  fi1uzind  14220  swrdnd  14376  sqrmo  14972  isprm2  16396  nprmdvds1  16420  oddprmdvds  16613  catsubcat  17563  funcestrcsetclem8  17873  funcestrcsetclem9  17874  fthestrcsetc  17876  fullestrcsetc  17877  funcsetcestrclem9  17889  fthsetcestrc  17891  fullsetcestrc  17892  pltletr  18070  issstrmgm  18346  mgm2nsgrplem3  18568  sgrp2nmndlem3  18573  fvcosymgeq  19046  sylow2alem2  19232  islss  20205  gzrngunitlem  20672  pjdm2  20927  assamulgscmlem2  21113  gsumply1subr  21414  dmatmul  21655  decpmatmullem  21929  monmat2matmon  21982  chpscmat  22000  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  isclo2  22248  fbasfip  23028  ufileu  23079  alexsubALTlem2  23208  cnextcn  23227  metustbl  23731  elntg2  27362  ushgredgedg  27605  ushgredgedgloop  27607  edgnbusgreu  27743  nb3grprlem1  27756  cusgrfilem1  27831  cusgrfilem2  27832  umgr2v2evtxel  27898  wlkcompim  28008  usgr2pth  28141  usgr2trlncrct  28180  wwlknp  28217  wlkiswwlks2lem3  28245  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wwlksnext  28267  2pthdlem1  28304  umgr2adedgwlkonALT  28321  umgr2wlkon  28324  elwspths2spth  28341  rusgr0edg  28347  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a  28371  clwwisshclwwslem  28387  loopclwwlkn1b  28415  clwwlkel  28419  clwwlkext2edg  28429  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknonwwlknonb  28479  uhgr3cyclexlem  28554  upgr4cycl4dv4e  28558  eupth2lem3lem4  28604  frgruhgr0v  28637  numclwwlk1lem2f1  28730  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  frgrogt3nreg  28770  5oalem6  30030  eigorthi  30208  adjbd1o  30456  dmdbr7ati  30795  fmla1  33358  satffunlem2lem2  33377  fundmpss  33749  funbreq  33753  scutbdaybnd2lim  34020  idinside  34395  bj-opelidres  35341  bj-eldiag2  35357  bj-fvimacnv0  35466  poimirlem32  35818  sdclem2  35909  fdc1  35913  ismgmOLD  36017  lsatcvatlem  37070  atnle  37338  cvratlem  37442  ispsubcl2N  37968  trlord  38590  diaelrnN  39066  cdlemm10N  39139  dochexmidlem7  39487  fsuppind  40286  3impexpbicom  42106  sbcim2g  42165  suctrALT2VD  42463  suctrALT2  42464  3impexpVD  42483  3impexpbicomVD  42484  sbcim2gVD  42502  csbeq2gVD  42519  csbsngVD  42520  ax6e2ndeqVD  42536  2sb5ndVD  42537  infxrunb3rnmpt  42975  lptioo2  43179  lptioo1  43180  funressnfv  44548  ffnafv  44674  tz6.12i-afv2  44746  iccpartiltu  44885  iccpartigtl  44886  icceuelpartlem  44898  fargshiftfo  44905  ichnreuop  44935  reupr  44985  bgoldbtbndlem2  45269  mgmpropd  45340  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  srhmsubc  45645  srhmsubcALTV  45663  nnolog2flm1  45947  prelrrx2b  46071  rrxlinec  46093  eenglngeehlnm  46096