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

Theorem biimpcd 239
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 235 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  biimpac  503  axc16i  2321  nelneq  2722  nelneq2  2723  nelne1  2886  nelne2  2887  nssne1  3646  nssne2  3647  psssstr  3697  iununi  4583  disjiun  4613  nbrne1  4642  nbrne2  4643  propeqop  4940  mosubopt  4942  issref  5478  tz7.7  5718  suctr  5777  tz6.12i  6181  ssimaex  6230  chfnrn  6294  fvn0ssdmfun  6316  ffnfv  6354  f1elima  6485  elovmpt3rab1  6858  limsssuc  7012  nnsuc  7044  peano5  7051  dftpos4  7331  odi  7619  fineqvlem  8134  pssnn  8138  ordunifi  8170  wdom2d  8445  r1pwss  8607  alephval3  8893  infdif  8991  cff1  9040  cofsmo  9051  axdc3lem2  9233  zorn2lem6  9283  cfpwsdom  9366  prub  9776  prnmadd  9779  1re  9999  letr  10091  dedekindle  10161  addid1  10176  negf1o  10420  negfi  10931  xrletr  11949  0fz1  12319  elfzmlbp  12407  leisorel  13198  elss2prb  13223  exprelprel  13226  fi1uzind  13234  fi1uzindOLD  13240  swrdnd  13386  swrdccatfn  13435  sqrmo  13942  isprm2  15338  nprmdvds1  15361  oddprmdvds  15550  catsubcat  16439  funcestrcsetclem8  16727  funcestrcsetclem9  16728  fthestrcsetc  16730  fullestrcsetc  16731  funcsetcestrclem9  16743  fthsetcestrc  16745  fullsetcestrc  16746  pltletr  16911  issstrmgm  17192  mgm2nsgrplem3  17347  sgrp2nmndlem3  17352  fvcosymgeq  17789  sylow2alem2  17973  islss  18875  assamulgscmlem2  19289  gsumply1subr  19544  gzrngunitlem  19751  pjdm2  19995  dmatmul  20243  decpmatmullem  20516  monmat2matmon  20569  chpscmat  20587  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  isclo2  20832  fbasfip  21612  ufileu  21663  alexsubALTlem2  21792  cnextcn  21811  metustbl  22311  ushgredgedg  26048  ushgredgedgloop  26050  edgnbusgreu  26190  nb3grprlem1  26203  cusgrfilem1  26272  cusgrfilem2  26273  umgr2v2evtxel  26338  wlkcompim  26431  usgr2pth  26563  usgr2trlncrct  26601  wwlknp  26637  wlkiswwlks2lem3  26660  wlkiswwlksupgr2  26666  wlklnwwlkln2lem  26671  wwlksnext  26691  2pthdlem1  26729  umgr2adedgwlkonALT  26746  umgr2wlkon  26749  elwspths2spth  26763  rusgr0edg  26769  isclwwlksnx  26790  clwlkclwwlklem2a1  26794  clwlkclwwlklem2a  26800  clwwlksel  26814  clwwlksext2edg  26823  wwlksext2clwwlk  26824  clwwisshclwwslem  26827  hashecclwwlksn1  26854  umgrhashecclwwlk  26855  clwlksfclwwlk  26862  clwlksf1clwwlklem2  26866  uhgr3cyclexlem  26941  upgr4cycl4dv4e  26945  eupth2lem3lem4  26991  frgruhgr0v  27027  frgreu  27083  fusgr2wsp2nb  27090  numclwlk1lem2f1  27116  numclwlk2lem2f  27125  numclwlk2lem2f1o  27127  frgrogt3nreg  27143  5oalem6  28406  eigorthi  28584  adjbd1o  28832  dmdbr7ati  29171  dfpo2  31406  fundmpss  31421  funbreq  31425  idinside  31886  bj-eldiag2  32764  poimirlem32  33112  sdclem2  33209  fdc1  33213  ismgmOLD  33320  lsatcvatlem  33855  atnle  34123  cvratlem  34226  ispsubcl2N  34752  trlord  35376  diaelrnN  35853  cdlemm10N  35926  dochexmidlem7  36274  3impexpbicom  38206  sbcim2g  38269  suctrALT2VD  38593  suctrALT2  38594  3impexpVD  38613  3impexpbicomVD  38614  sbcim2gVD  38633  csbeq2gVD  38650  csbsngVD  38651  ax6e2ndeqVD  38667  2sb5ndVD  38668  infxrunb3rnmpt  39154  lptioo2  39299  lptioo1  39300  funressnfv  40542  ffnafv  40585  iccpartiltu  40686  iccpartigtl  40687  icceuelpartlem  40699  fargshiftfo  40706  bgoldbtbndlem2  41013  mgmpropd  41093  rngcinv  41299  rngcinvALTV  41311  ringcinv  41350  ringcinvALTV  41374  srhmsubc  41394  srhmsubcALTV  41412  nnolog2flm1  41706
  Copyright terms: Public domain W3C validator