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

Theorem biimpcd 238
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 234 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  biimpac  502  axc16i  2310  nelneq  2712  nelneq2  2713  nelne1  2878  nelne2  2879  nssne1  3624  nssne2  3625  psssstr  3675  iununi  4541  disjiun  4568  nbrne1  4597  nbrne2  4598  mosubopt  4888  issref  5415  tz7.7  5652  suctr  5711  tz6.12i  6109  ssimaex  6158  chfnrn  6221  fvn0ssdmfun  6243  ffnfv  6280  f1elima  6399  elovmpt3rab1  6769  limsssuc  6920  nnsuc  6952  peano5  6959  dftpos4  7236  odi  7524  fineqvlem  8037  pssnn  8041  ordunifi  8073  wdom2d  8346  r1pwss  8508  alephval3  8794  infdif  8892  cff1  8941  cofsmo  8952  axdc3lem2  9134  zorn2lem6  9184  cfpwsdom  9263  prub  9673  prnmadd  9676  1re  9896  letr  9983  dedekindle  10053  addid1  10068  negf1o  10312  negfi  10823  xrletr  11827  0fz1  12190  elfzmlbp  12277  leisorel  13056  elss2prb  13076  exprelprel  13079  fi1uzind  13083  fi1uzindOLD  13089  swrdnd  13233  swrdccatfn  13282  sqrmo  13789  isprm2  15182  nprmdvds1  15205  oddprmdvds  15394  catsubcat  16271  funcestrcsetclem8  16559  funcestrcsetclem9  16560  fthestrcsetc  16562  fullestrcsetc  16563  funcsetcestrclem9  16575  fthsetcestrc  16577  fullsetcestrc  16578  pltletr  16743  issstrmgm  17024  mgm2nsgrplem3  17179  sgrp2nmndlem3  17184  fvcosymgeq  17621  sylow2alem2  17805  islss  18705  assamulgscmlem2  19119  gsumply1subr  19374  gzrngunitlem  19579  pjdm2  19822  dmatmul  20070  decpmatmullem  20343  monmat2matmon  20396  chpscmat  20414  chfacfscmulgsum  20432  chfacfpmmulgsum  20436  isclo2  20650  fbasfip  21430  ufileu  21481  alexsubALTlem2  21610  cnextcn  21629  metustbl  22129  usgrarnedg1  25712  nbgraf1olem3  25766  nbgraf1olem5  25768  nb3graprlem1  25774  cusgrafilem2  25802  wlkn0  25849  fargshiftfo  25960  3v3e3cycl1  25966  4cycl4v4e  25988  4cycl4dv4e  25990  wlkiswwlk2lem3  26015  wlklniswwlkn1  26021  wlklniswwlkn2  26022  wwlknext  26046  clwwlknimp  26098  clwlkisclwwlklem2a1  26101  clwlkisclwwlklem2a  26107  clwwlkel  26115  clwwlkext2edg  26124  wwlkext2clwwlk  26125  clwwisshclwwlem  26128  hashecclwwlkn1  26155  usghashecclwwlk  26156  clwlkfclwwlk  26165  clwlkf1clwwlklem2  26168  el2wlkonot  26190  el2wlkonotot1  26195  frgrancvvdeqlemA  26358  frgrancvvdeqlemC  26360  frgraeu  26375  numclwlk2lem2f  26424  numclwlk2lem2f1o  26426  frgraogt3nreg  26441  5oalem6  27696  eigorthi  27874  adjbd1o  28122  dmdbr7ati  28461  dfpo2  30692  fundmpss  30704  funbreq  30708  idinside  31155  bj-eldiag2  32063  poimirlem32  32405  sdclem2  32502  fdc1  32506  ismgmOLD  32613  lsatcvatlem  33148  atnle  33416  cvratlem  33519  ispsubcl2N  34045  trlord  34669  diaelrnN  35146  cdlemm10N  35219  dochexmidlem7  35567  3impexpbicom  37500  sbcim2g  37563  suctrALT2VD  37887  suctrALT2  37888  3impexpVD  37907  3impexpbicomVD  37908  sbcim2gVD  37927  csbeq2gVD  37944  csbsngVD  37945  ax6e2ndeqVD  37961  2sb5ndVD  37962  lptioo2  38492  lptioo1  38493  funressnfv  39651  ffnafv  39695  iccpartiltu  39755  iccpartigtl  39756  icceuelpartlem  39768  bgoldbtbndlem2  40017  propeqop  40116  ushgredgedga  40448  ushgredgedgaloop  40450  edgnbusgreu  40587  nb3grprlem1  40600  cusgrfilem1  40663  cusgrfilem2  40664  umgr2v2evtxel  40730  1wlkcompim  40828  usgr2trlncrct  41001  wwlknp  41037  1wlkiswwlks2lem3  41060  1wlkiswwlksupgr2  41066  1wlklnwwlkln2lem  41071  wwlksnext  41091  2pthdlem1  41129  umgr2adedgwlkonALT  41146  umgr2wlkon  41149  elwspths2spth  41163  rusgr0edg  41168  isclwwlksnx  41189  clwlkclwwlklem2a1  41193  clwlkclwwlklem2a  41199  clwwlksel  41213  clwwlksext2edg  41222  wwlksext2clwwlk  41223  clwwisshclwwslem  41226  hashecclwwlksn1  41253  umgrhashecclwwlk  41254  clwlksfclwwlk  41261  clwlksf1clwwlklem2  41265  uhgr3cyclexlem  41340  upgr4cycl4dv4e  41344  eupth2lem3lem4  41391  frgruhgr0v  41427  frgreu  41483  fusgr2wsp2nb  41490  av-numclwlk1lem2f1  41516  av-numclwlk2lem2f  41525  av-numclwlk2lem2f1o  41527  av-frgraogt3nreg  41543  mgmpropd  41557  rngcinv  41765  rngcinvALTV  41777  ringcinv  41816  ringcinvALTV  41840  srhmsubc  41860  srhmsubcALTV  41879  nnolog2flm1  42174
  Copyright terms: Public domain W3C validator