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  502  axc16i  2353  nelneq  2754  nelneq2  2755  nelne1  2919  nelne2  2920  nssne1  3694  nssne2  3695  psssstr  3746  prproe  4466  iununi  4642  disjiun  4672  nbrne1  4704  nbrne2  4705  propeqop  4999  mosubopt  5001  issref  5544  tz7.7  5787  suctr  5846  tz6.12i  6252  ssimaex  6302  chfnrn  6368  fvn0ssdmfun  6390  ffnfv  6428  f1elima  6560  elovmpt3rab1  6935  limsssuc  7092  nnsuc  7124  peano5  7131  dftpos4  7416  odi  7704  fineqvlem  8215  pssnn  8219  ordunifi  8251  wdom2d  8526  r1pwss  8685  alephval3  8971  infdif  9069  cff1  9118  cofsmo  9129  axdc3lem2  9311  zorn2lem6  9361  cfpwsdom  9444  prub  9854  prnmadd  9857  1re  10077  letr  10169  dedekindle  10239  addid1  10254  negf1o  10498  negfi  11009  xrletr  12027  0fz1  12399  elfzmlbp  12489  leisorel  13282  elss2prb  13307  exprelprel  13309  fi1uzind  13317  swrdnd  13478  swrdccatfn  13528  sqrmo  14036  isprm2  15442  nprmdvds1  15465  oddprmdvds  15654  catsubcat  16546  funcestrcsetclem8  16834  funcestrcsetclem9  16835  fthestrcsetc  16837  fullestrcsetc  16838  funcsetcestrclem9  16850  fthsetcestrc  16852  fullsetcestrc  16853  pltletr  17018  issstrmgm  17299  mgm2nsgrplem3  17454  sgrp2nmndlem3  17459  fvcosymgeq  17895  sylow2alem2  18079  islss  18983  assamulgscmlem2  19397  gsumply1subr  19652  gzrngunitlem  19859  pjdm2  20103  dmatmul  20351  decpmatmullem  20624  monmat2matmon  20677  chpscmat  20695  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  isclo2  20940  fbasfip  21719  ufileu  21770  alexsubALTlem2  21899  cnextcn  21918  metustbl  22418  ushgredgedg  26166  ushgredgedgloop  26168  edgnbusgreu  26313  nb3grprlem1  26326  cusgrfilem1  26407  cusgrfilem2  26408  umgr2v2evtxel  26474  wlkcompim  26583  usgr2pth  26716  usgr2trlncrct  26754  wwlknp  26791  wlkiswwlks2lem3  26825  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wwlksnext  26856  2pthdlem1  26895  umgr2adedgwlkonALT  26912  umgr2wlkon  26915  elwspths2spth  26934  rusgr0edg  26940  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a  26964  clwwisshclwwslem  26971  loopclwwlkn1b  27005  clwwlkel  27009  clwwlkext2edg  27020  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwlksf1clwwlklem2  27053  uhgr3cyclexlem  27159  upgr4cycl4dv4e  27163  eupth2lem3lem4  27209  frgruhgr0v  27243  numclwlk1lem2f1  27347  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  frgrogt3nreg  27384  5oalem6  28646  eigorthi  28824  adjbd1o  29072  dmdbr7ati  29411  dfpo2  31771  fundmpss  31790  funbreq  31794  idinside  32316  bj-eldiag2  33222  poimirlem32  33571  sdclem2  33668  fdc1  33672  ismgmOLD  33779  lsatcvatlem  34654  atnle  34922  cvratlem  35025  ispsubcl2N  35551  trlord  36174  diaelrnN  36651  cdlemm10N  36724  dochexmidlem7  37072  3impexpbicom  39002  sbcim2g  39065  suctrALT2VD  39385  suctrALT2  39386  3impexpVD  39405  3impexpbicomVD  39406  sbcim2gVD  39425  csbeq2gVD  39442  csbsngVD  39443  ax6e2ndeqVD  39459  2sb5ndVD  39460  infxrunb3rnmpt  39968  lptioo2  40181  lptioo1  40182  funressnfv  41529  ffnafv  41572  iccpartiltu  41683  iccpartigtl  41684  icceuelpartlem  41696  fargshiftfo  41703  bgoldbtbndlem2  42019  mgmpropd  42100  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  srhmsubc  42401  srhmsubcALTV  42419  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator