MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpcd Structured version   Visualization version   GIF version

Theorem biimpcd 250
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
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
2 biimpcd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5ibcom 246 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  biimpac  479  axc16i  2455  nelneq  2941  nelneq2  2942  nelne1OLD  3118  nelne2OLD  3120  nssne1  4030  nssne2  4031  psssstr  4086  prproe  4834  iununi  5017  disjiun  5049  nbrne1  5081  nbrne2  5082  propeqop  5393  mosubopt  5396  relsnb  5673  relcnvtrg  6116  reuop  6141  tz7.7  6214  suctr  6271  tz6.12i  6692  ssimaex  6744  chfnrn  6814  fvn0ssdmfun  6837  ffnfv  6877  f1elima  7018  elovmpt3rab1  7398  limsssuc  7556  nnsuc  7588  peano5  7596  dftpos4  7905  odi  8198  fineqvlem  8724  pssnn  8728  ordunifi  8760  wdom2d  9036  r1pwss  9205  alephval3  9528  infdif  9623  cff1  9672  cofsmo  9683  axdc3lem2  9865  zorn2lem6  9915  cfpwsdom  9998  prub  10408  prnmadd  10411  1re  10633  letr  10726  dedekindle  10796  addid1  10812  negf1o  11062  negfi  11581  xrletr  12544  0fz1  12920  elfzmlbp  13011  leisorel  13811  elss2prb  13838  exprelprel  13840  fi1uzind  13848  swrdnd  14009  sqrmo  14604  isprm2  16018  nprmdvds1  16042  oddprmdvds  16231  catsubcat  17101  funcestrcsetclem8  17389  funcestrcsetclem9  17390  fthestrcsetc  17392  fullestrcsetc  17393  funcsetcestrclem9  17405  fthsetcestrc  17407  fullsetcestrc  17408  pltletr  17573  issstrmgm  17854  mgm2nsgrplem3  18020  sgrp2nmndlem3  18025  fvcosymgeq  18479  sylow2alem2  18665  islss  19628  assamulgscmlem2  20050  gsumply1subr  20321  gzrngunitlem  20528  pjdm2  20773  dmatmul  21024  decpmatmullem  21297  monmat2matmon  21350  chpscmat  21368  chfacfscmulgsum  21386  chfacfpmmulgsum  21390  isclo2  21614  fbasfip  22394  ufileu  22445  alexsubALTlem2  22574  cnextcn  22593  metustbl  23093  elntg2  26687  ushgredgedg  26927  ushgredgedgloop  26929  edgnbusgreu  27065  nb3grprlem1  27078  cusgrfilem1  27153  cusgrfilem2  27154  umgr2v2evtxel  27220  wlkcompim  27329  usgr2pth  27461  usgr2trlncrct  27500  wwlknp  27537  wlkiswwlks2lem3  27565  wlkiswwlksupgr2  27571  wlklnwwlkln2lem  27576  wwlksnext  27587  2pthdlem1  27625  umgr2adedgwlkonALT  27642  umgr2wlkon  27645  elwspths2spth  27662  rusgr0edg  27668  clwlkclwwlklem2a1  27686  clwlkclwwlklem2a  27692  clwwisshclwwslem  27708  loopclwwlkn1b  27736  clwwlkel  27741  clwwlkext2edg  27751  hashecclwwlkn1  27772  umgrhashecclwwlk  27773  clwwlknonwwlknonb  27801  uhgr3cyclexlem  27876  upgr4cycl4dv4e  27880  eupth2lem3lem4  27926  frgruhgr0v  27959  numclwwlk1lem2f1  28052  numclwlk2lem2f  28072  numclwlk2lem2f1o  28074  frgrogt3nreg  28092  5oalem6  29352  eigorthi  29530  adjbd1o  29778  dmdbr7ati  30117  fmla1  32520  satffunlem2lem2  32539  dfpo2  32877  fundmpss  32895  funbreq  32899  idinside  33431  bj-opelidres  34334  bj-eldiag2  34350  bj-imdirid  34356  bj-fvimacnv0  34445  poimirlem32  34793  sdclem2  34887  fdc1  34891  ismgmOLD  34998  lsatcvatlem  36054  atnle  36322  cvratlem  36426  ispsubcl2N  36952  trlord  37574  diaelrnN  38050  cdlemm10N  38123  dochexmidlem7  38471  3impexpbicom  40680  sbcim2g  40739  suctrALT2VD  41037  suctrALT2  41038  3impexpVD  41057  3impexpbicomVD  41058  sbcim2gVD  41076  csbeq2gVD  41093  csbsngVD  41094  ax6e2ndeqVD  41110  2sb5ndVD  41111  infxrunb3rnmpt  41569  lptioo2  41779  lptioo1  41780  funressnfv  43146  ffnafv  43238  tz6.12i-afv2  43310  iccpartiltu  43416  iccpartigtl  43417  icceuelpartlem  43429  fargshiftfo  43436  ichnreuop  43468  reupr  43518  bgoldbtbndlem2  43805  mgmpropd  43876  rngcinv  44086  rngcinvALTV  44098  ringcinv  44137  ringcinvALTV  44161  srhmsubc  44181  srhmsubcALTV  44199  nnolog2flm1  44484  prelrrx2b  44535  rrxlinec  44557  eenglngeehlnm  44560
  Copyright terms: Public domain W3C validator