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  478  axc16i  2434  nelneq  2856  nelneq2  2857  r19.35  3107  nssne1  4044  nssne2  4045  psssstr  4106  prproe  4906  iununi  5102  disjiun  5135  nbrne1  5167  nbrne2  5168  propeqop  5507  mosubopt  5510  relsnb  5802  relcnvtrg  6265  reuop  6292  dfpo2  6295  tz7.7  6390  suctr  6450  tz6.12i  6919  ssimaex  6976  chfnrn  7050  fvn0ssdmfun  7076  ffnfv  7120  f1elima  7265  elovmpt3rab1  7670  limsssuc  7843  nnsuc  7877  peano5  7888  peano5OLD  7889  dftpos4  8236  odi  8585  pssnn  9174  fineqvlem  9268  pssnnOLD  9271  ordunifi  9299  wdom2d  9581  r1pwss  9785  alephval3  10111  infdif  10210  cff1  10259  cofsmo  10270  axdc3lem2  10452  zorn2lem6  10502  cfpwsdom  10585  prub  10995  prnmadd  10998  1re  11221  letr  11315  dedekindle  11385  addrid  11401  negf1o  11651  negfi  12170  xrletr  13144  0fz1  13528  elfzmlbp  13619  leisorel  14428  elss2prb  14455  exprelprel  14457  fi1uzind  14465  swrdnd  14611  sqrmo  15205  isprm2  16626  nprmdvds1  16650  oddprmdvds  16843  catsubcat  17796  funcestrcsetclem8  18109  funcestrcsetclem9  18110  fthestrcsetc  18112  fullestrcsetc  18113  funcsetcestrclem9  18125  fthsetcestrc  18127  fullsetcestrc  18128  pltletr  18306  mgmpropd  18582  issstrmgm  18584  mgm2nsgrplem3  18843  sgrp2nmndlem3  18848  fvcosymgeq  19345  sylow2alem2  19534  rngcinv  20529  srhmsubc  20572  islss  20777  gzrngunitlem  21299  pjdm2  21576  assamulgscmlem2  21764  gsumply1subr  22076  dmatmul  22319  decpmatmullem  22593  monmat2matmon  22646  chpscmat  22664  chfacfscmulgsum  22682  chfacfpmmulgsum  22686  isclo2  22912  fbasfip  23692  ufileu  23743  alexsubALTlem2  23872  cnextcn  23891  metustbl  24395  scutbdaybnd2lim  27664  addsprop  27807  elntg2  28677  ushgredgedg  28920  ushgredgedgloop  28922  edgnbusgreu  29058  nb3grprlem1  29071  cusgrfilem1  29146  cusgrfilem2  29147  umgr2v2evtxel  29213  wlkcompim  29323  usgr2pth  29455  usgr2trlncrct  29494  wwlknp  29531  wlkiswwlks2lem3  29559  wlkiswwlksupgr2  29565  wlklnwwlkln2lem  29570  wwlksnext  29581  2pthdlem1  29618  umgr2adedgwlkonALT  29635  umgr2wlkon  29638  elwspths2spth  29655  rusgr0edg  29661  clwlkclwwlklem2a1  29679  clwlkclwwlklem2a  29685  clwwisshclwwslem  29701  loopclwwlkn1b  29729  clwwlkel  29733  clwwlkext2edg  29743  hashecclwwlkn1  29764  umgrhashecclwwlk  29765  clwwlknonwwlknonb  29793  uhgr3cyclexlem  29868  upgr4cycl4dv4e  29872  eupth2lem3lem4  29918  frgruhgr0v  29951  numclwwlk1lem2f1  30044  numclwlk2lem2f  30064  numclwlk2lem2f1o  30066  frgrogt3nreg  30084  5oalem6  31346  eigorthi  31524  adjbd1o  31772  dmdbr7ati  32111  fmla1  34843  satffunlem2lem2  34862  fundmpss  35209  funbreq  35212  idinside  35527  bj-opelidres  36508  bj-eldiag2  36524  bj-fvimacnv0  36633  poimirlem32  36986  sdclem2  37076  fdc1  37080  ismgmOLD  37184  lsatcvatlem  38385  atnle  38653  cvratlem  38758  ispsubcl2N  39284  trlord  39906  diaelrnN  40382  cdlemm10N  40455  dochexmidlem7  40803  fsuppind  41627  3impexpbicom  43705  sbcim2g  43764  suctrALT2VD  44062  suctrALT2  44063  3impexpVD  44082  3impexpbicomVD  44083  sbcim2gVD  44101  csbeq2gVD  44118  csbsngVD  44119  ax6e2ndeqVD  44135  2sb5ndVD  44136  infxrunb3rnmpt  44599  lptioo2  44808  lptioo1  44809  funressnfv  46214  ffnafv  46340  tz6.12i-afv2  46412  iccpartiltu  46551  iccpartigtl  46552  icceuelpartlem  46564  fargshiftfo  46571  ichnreuop  46601  reupr  46651  bgoldbtbndlem2  46935  rngcinvALTV  47115  srhmsubcALTV  47164  nnolog2flm1  47440  prelrrx2b  47564  rrxlinec  47586  eenglngeehlnm  47589