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

Theorem biimpcd 240
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 236 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  biimpac  470  axc16i  2416  nelneq  2868  nelneq2  2869  nelne1  3033  nelne2  3034  nssne1  3821  nssne2  3822  psssstr  3874  prproe  4592  iununi  4767  disjiun  4797  nbrne1  4828  nbrne2  4829  propeqop  5128  mosubopt  5131  idrefOLD  5692  tz7.7  5934  suctr  5991  tz6.12i  6401  ssimaex  6452  chfnrn  6518  fvn0ssdmfun  6540  ffnfv  6578  f1elima  6712  elovmpt3rab1  7091  limsssuc  7248  nnsuc  7280  peano5  7287  dftpos4  7574  odi  7864  fineqvlem  8381  pssnn  8385  ordunifi  8417  wdom2d  8692  r1pwss  8862  alephval3  9184  infdif  9284  cff1  9333  cofsmo  9344  axdc3lem2  9526  zorn2lem6  9576  cfpwsdom  9659  prub  10069  prnmadd  10072  1re  10293  letr  10385  dedekindle  10455  addid1  10470  negf1o  10714  negfi  11225  xrletr  12191  0fz1  12568  elfzmlbp  12658  leisorel  13445  elss2prb  13470  exprelprel  13472  fi1uzind  13480  swrdnd  13634  swrdccatfn  13728  sqrmo  14277  isprm2  15675  nprmdvds1  15697  oddprmdvds  15886  catsubcat  16764  funcestrcsetclem8  17053  funcestrcsetclem9  17054  fthestrcsetc  17056  fullestrcsetc  17057  funcsetcestrclem9  17069  fthsetcestrc  17071  fullsetcestrc  17072  pltletr  17237  issstrmgm  17518  mgm2nsgrplem3  17674  sgrp2nmndlem3  17679  fvcosymgeq  18112  sylow2alem2  18297  islss  19204  assamulgscmlem2  19623  gsumply1subr  19877  gzrngunitlem  20084  pjdm2  20331  dmatmul  20580  decpmatmullem  20855  monmat2matmon  20908  chpscmat  20926  chfacfscmulgsum  20944  chfacfpmmulgsum  20948  isclo2  21172  fbasfip  21951  ufileu  22002  alexsubALTlem2  22131  cnextcn  22150  metustbl  22650  ushgredgedg  26399  ushgredgedgloop  26401  ushgredgedgloopOLD  26402  edgnbusgreu  26547  edgnbusgreuOLD  26548  nb3grprlem1  26561  cusgrfilem1  26642  cusgrfilem2  26643  umgr2v2evtxel  26709  wlkcompim  26818  usgr2pth  26952  usgr2trlncrct  26991  wwlknp  27028  wlkiswwlks2lem3  27062  wlkiswwlksupgr2  27068  wlklnwwlkln2lem  27074  wwlksnext  27096  2pthdlem1  27153  umgr2adedgwlkonALT  27170  umgr2wlkon  27173  elwspths2spth  27192  rusgr0edg  27198  clwlkclwwlklem2a1  27219  clwlkclwwlklem2a  27225  clwwisshclwwslem  27250  loopclwwlkn1b  27285  clwwlkel  27289  clwwlkext2edg  27306  wwlksext2clwwlk  27307  wwlksext2clwwlkOLD  27308  hashecclwwlkn1  27329  umgrhashecclwwlk  27330  clwlksfclwwlkOLD  27337  clwlksf1clwwlklem2OLD  27341  uhgr3cyclexlem  27459  upgr4cycl4dv4e  27463  eupth2lem3lem4  27509  frgruhgr0v  27543  numclwwlk1lem2f1  27649  numclwwlk1lem2f1OLD  27654  numclwlk2lem2f  27681  numclwlk2lem2f1o  27683  numclwlk2lem2fOLD  27684  numclwlk2lem2f1oOLD  27686  numclwlk2lem2fOLDOLD  27692  numclwlk2lem2f1oOLDOLD  27694  frgrogt3nreg  27713  5oalem6  28974  eigorthi  29152  adjbd1o  29400  dmdbr7ati  29739  dfpo2  32090  fundmpss  32109  funbreq  32113  idinside  32635  bj-eldiag2  33526  poimirlem32  33865  sdclem2  33960  fdc1  33964  ismgmOLD  34071  lsatcvatlem  35005  atnle  35273  cvratlem  35377  ispsubcl2N  35903  trlord  36525  diaelrnN  37001  cdlemm10N  37074  dochexmidlem7  37422  3impexpbicom  39357  sbcim2g  39416  suctrALT2VD  39724  suctrALT2  39725  3impexpVD  39744  3impexpbicomVD  39745  sbcim2gVD  39763  csbeq2gVD  39780  csbsngVD  39781  ax6e2ndeqVD  39797  2sb5ndVD  39798  infxrunb3rnmpt  40292  lptioo2  40501  lptioo1  40502  funressnfv  41820  ffnafv  41919  tz6.12i-afv2  41991  iccpartiltu  42092  iccpartigtl  42093  icceuelpartlem  42105  fargshiftfo  42112  bgoldbtbndlem2  42370  mgmpropd  42444  rngcinv  42650  rngcinvALTV  42662  ringcinv  42701  ringcinvALTV  42725  srhmsubc  42745  srhmsubcALTV  42763  nnolog2flm1  43053
  Copyright terms: Public domain W3C validator