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  2453  nelneq  2937  nelneq2  2938  nelne1OLD  3114  nelne2OLD  3116  nssne1  4026  nssne2  4027  psssstr  4082  prproe  4830  iununi  5013  disjiun  5045  nbrne1  5077  nbrne2  5078  propeqop  5389  mosubopt  5392  relsnb  5669  relcnvtrg  6113  reuop  6138  tz7.7  6211  suctr  6268  tz6.12i  6690  ssimaex  6742  chfnrn  6812  fvn0ssdmfun  6835  ffnfv  6875  f1elima  7012  elovmpt3rab1  7394  limsssuc  7553  nnsuc  7585  peano5  7593  dftpos4  7902  odi  8195  fineqvlem  8721  pssnn  8725  ordunifi  8757  wdom2d  9033  r1pwss  9202  alephval3  9525  infdif  9620  cff1  9669  cofsmo  9680  axdc3lem2  9862  zorn2lem6  9912  cfpwsdom  9995  prub  10405  prnmadd  10408  1re  10630  letr  10723  dedekindle  10793  addid1  10809  negf1o  11059  negfi  11578  xrletr  12541  0fz1  12917  elfzmlbp  13008  leisorel  13808  elss2prb  13835  exprelprel  13837  fi1uzind  13845  swrdnd  14006  sqrmo  14601  isprm2  16016  nprmdvds1  16040  oddprmdvds  16229  catsubcat  17099  funcestrcsetclem8  17387  funcestrcsetclem9  17388  fthestrcsetc  17390  fullestrcsetc  17391  funcsetcestrclem9  17403  fthsetcestrc  17405  fullsetcestrc  17406  pltletr  17571  issstrmgm  17853  mgm2nsgrplem3  18025  sgrp2nmndlem3  18030  fvcosymgeq  18488  sylow2alem2  18674  islss  19637  assamulgscmlem2  20059  gsumply1subr  20332  gzrngunitlem  20540  pjdm2  20785  dmatmul  21036  decpmatmullem  21309  monmat2matmon  21362  chpscmat  21380  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  isclo2  21626  fbasfip  22406  ufileu  22457  alexsubALTlem2  22586  cnextcn  22605  metustbl  23105  elntg2  26699  ushgredgedg  26939  ushgredgedgloop  26941  edgnbusgreu  27077  nb3grprlem1  27090  cusgrfilem1  27165  cusgrfilem2  27166  umgr2v2evtxel  27232  wlkcompim  27341  usgr2pth  27473  usgr2trlncrct  27512  wwlknp  27549  wlkiswwlks2lem3  27577  wlkiswwlksupgr2  27583  wlklnwwlkln2lem  27588  wwlksnext  27599  2pthdlem1  27637  umgr2adedgwlkonALT  27654  umgr2wlkon  27657  elwspths2spth  27674  rusgr0edg  27680  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a  27704  clwwisshclwwslem  27720  loopclwwlkn1b  27748  clwwlkel  27753  clwwlkext2edg  27763  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknonwwlknonb  27813  uhgr3cyclexlem  27888  upgr4cycl4dv4e  27892  eupth2lem3lem4  27938  frgruhgr0v  27971  numclwwlk1lem2f1  28064  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  frgrogt3nreg  28104  5oalem6  29364  eigorthi  29542  adjbd1o  29790  dmdbr7ati  30129  fmla1  32532  satffunlem2lem2  32551  dfpo2  32889  fundmpss  32907  funbreq  32911  idinside  33443  bj-opelidres  34346  bj-eldiag2  34362  bj-imdirid  34368  bj-fvimacnv0  34457  poimirlem32  34806  sdclem2  34900  fdc1  34904  ismgmOLD  35011  lsatcvatlem  36067  atnle  36335  cvratlem  36439  ispsubcl2N  36965  trlord  37587  diaelrnN  38063  cdlemm10N  38136  dochexmidlem7  38484  3impexpbicom  40693  sbcim2g  40752  suctrALT2VD  41050  suctrALT2  41051  3impexpVD  41070  3impexpbicomVD  41071  sbcim2gVD  41089  csbeq2gVD  41106  csbsngVD  41107  ax6e2ndeqVD  41123  2sb5ndVD  41124  infxrunb3rnmpt  41582  lptioo2  41792  lptioo1  41793  funressnfv  43159  ffnafv  43251  tz6.12i-afv2  43323  iccpartiltu  43429  iccpartigtl  43430  icceuelpartlem  43442  fargshiftfo  43449  ichnreuop  43481  reupr  43531  bgoldbtbndlem2  43818  mgmpropd  43889  rngcinv  44150  rngcinvALTV  44162  ringcinv  44201  ringcinvALTV  44225  srhmsubc  44245  srhmsubcALTV  44263  nnolog2flm1  44548  prelrrx2b  44599  rrxlinec  44621  eenglngeehlnm  44624
  Copyright terms: Public domain W3C validator