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  480  axc16i  2436  nelneq  2858  nelneq2  2859  r19.35  3109  nssne1  4045  nssne2  4046  psssstr  4107  prproe  4907  iununi  5103  disjiun  5136  nbrne1  5168  nbrne2  5169  propeqop  5508  mosubopt  5511  relsnb  5803  relcnvtrg  6266  reuop  6293  dfpo2  6296  tz7.7  6391  suctr  6451  tz6.12i  6920  ssimaex  6977  chfnrn  7051  fvn0ssdmfun  7077  ffnfv  7118  f1elima  7262  elovmpt3rab1  7666  limsssuc  7839  nnsuc  7873  peano5  7884  peano5OLD  7885  dftpos4  8230  odi  8579  pssnn  9168  fineqvlem  9262  pssnnOLD  9265  ordunifi  9293  wdom2d  9575  r1pwss  9779  alephval3  10105  infdif  10204  cff1  10253  cofsmo  10264  axdc3lem2  10446  zorn2lem6  10496  cfpwsdom  10579  prub  10989  prnmadd  10992  1re  11214  letr  11308  dedekindle  11378  addrid  11394  negf1o  11644  negfi  12163  xrletr  13137  0fz1  13521  elfzmlbp  13612  leisorel  14421  elss2prb  14448  exprelprel  14450  fi1uzind  14458  swrdnd  14604  sqrmo  15198  isprm2  16619  nprmdvds1  16643  oddprmdvds  16836  catsubcat  17789  funcestrcsetclem8  18099  funcestrcsetclem9  18100  fthestrcsetc  18102  fullestrcsetc  18103  funcsetcestrclem9  18115  fthsetcestrc  18117  fullsetcestrc  18118  pltletr  18296  issstrmgm  18572  mgm2nsgrplem3  18801  sgrp2nmndlem3  18806  fvcosymgeq  19297  sylow2alem2  19486  islss  20545  gzrngunitlem  21010  pjdm2  21266  assamulgscmlem2  21454  gsumply1subr  21756  dmatmul  21999  decpmatmullem  22273  monmat2matmon  22326  chpscmat  22344  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  isclo2  22592  fbasfip  23372  ufileu  23423  alexsubALTlem2  23552  cnextcn  23571  metustbl  24075  scutbdaybnd2lim  27319  addsprop  27462  elntg2  28274  ushgredgedg  28517  ushgredgedgloop  28519  edgnbusgreu  28655  nb3grprlem1  28668  cusgrfilem1  28743  cusgrfilem2  28744  umgr2v2evtxel  28810  wlkcompim  28920  usgr2pth  29052  usgr2trlncrct  29091  wwlknp  29128  wlkiswwlks2lem3  29156  wlkiswwlksupgr2  29162  wlklnwwlkln2lem  29167  wwlksnext  29178  2pthdlem1  29215  umgr2adedgwlkonALT  29232  umgr2wlkon  29235  elwspths2spth  29252  rusgr0edg  29258  clwlkclwwlklem2a1  29276  clwlkclwwlklem2a  29282  clwwisshclwwslem  29298  loopclwwlkn1b  29326  clwwlkel  29330  clwwlkext2edg  29340  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  clwwlknonwwlknonb  29390  uhgr3cyclexlem  29465  upgr4cycl4dv4e  29469  eupth2lem3lem4  29515  frgruhgr0v  29548  numclwwlk1lem2f1  29641  numclwlk2lem2f  29661  numclwlk2lem2f1o  29663  frgrogt3nreg  29681  5oalem6  30943  eigorthi  31121  adjbd1o  31369  dmdbr7ati  31708  fmla1  34409  satffunlem2lem2  34428  fundmpss  34769  funbreq  34772  idinside  35087  bj-opelidres  36090  bj-eldiag2  36106  bj-fvimacnv0  36215  poimirlem32  36568  sdclem2  36658  fdc1  36662  ismgmOLD  36766  lsatcvatlem  37967  atnle  38235  cvratlem  38340  ispsubcl2N  38866  trlord  39488  diaelrnN  39964  cdlemm10N  40037  dochexmidlem7  40385  fsuppind  41210  3impexpbicom  43288  sbcim2g  43347  suctrALT2VD  43645  suctrALT2  43646  3impexpVD  43665  3impexpbicomVD  43666  sbcim2gVD  43684  csbeq2gVD  43701  csbsngVD  43702  ax6e2ndeqVD  43718  2sb5ndVD  43719  infxrunb3rnmpt  44186  lptioo2  44395  lptioo1  44396  funressnfv  45801  ffnafv  45927  tz6.12i-afv2  45999  iccpartiltu  46138  iccpartigtl  46139  icceuelpartlem  46151  fargshiftfo  46158  ichnreuop  46188  reupr  46238  bgoldbtbndlem2  46522  mgmpropd  46593  rngcinv  46927  rngcinvALTV  46939  srhmsubc  47022  srhmsubcALTV  47040  nnolog2flm1  47324  prelrrx2b  47448  rrxlinec  47470  eenglngeehlnm  47473