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

Theorem pm2.43i 52
Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 56. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43i.1 (𝜑 → (𝜑𝜓))
Assertion
Ref Expression
pm2.43i (𝜑𝜓)

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 pm2.43i.1 . 2 (𝜑 → (𝜑𝜓))
31, 2mpd 15 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  sylc  65  pm2.18  122  impbid  202  ibi  256  anidms  680  3imp3i2anOLD  1438  tbw-bijust  1772  tbw-negdf  1773  equid  2094  nf5di  2266  nfdiOLD  2370  hbae  2457  vtoclgaf  3411  vtocl2gaf  3413  vtocl3gaf  3415  vtocl4ga  3418  elinti  4637  copsexg  5104  vtoclr  5321  ssrelrn  5470  issref  5667  relresfld  5823  tz7.7  5910  elfvmptrab1  6468  tfisi  7224  bropopvvv  7424  f1o2ndf1  7454  suppimacnv  7475  brovex  7518  tfrlem9  7651  tfrlem11  7654  odi  7830  nndi  7874  sbth  8247  sdomdif  8275  zorn2lem7  9536  alephexp2  9615  addcanpi  9933  mulcanpi  9934  indpi  9941  prcdnq  10027  reclem2pr  10082  lediv2a  11129  nn01to3  11994  fi1uzind  13491  cshwlen  13765  cshwidxmodr  13770  rlimres  14508  ndvdssub  15355  bitsinv1  15386  nn0seqcvgd  15505  modprm0  15732  setsstruct  16120  initoeu2  16887  symgfixelsi  18075  symgfixfo  18079  uvcendim  20408  slesolex  20710  pm2mpf1  20826  mp2pm2mplem4  20836  fiinopn  20928  jensenlem2  24934  umgrupgr  26218  uspgrushgr  26290  uspgrupgr  26291  usgruspgr  26293  usgredg2vlem2  26338  cplgrop  26564  lfgrwlkprop  26815  2pthnloop  26858  usgr2pthlem  26890  elwwlks2  27109  clwlkclwwlklem2fv2  27140  eleclclwwlkn  27228  hashecclwwlkn1  27229  umgrhashecclwwlk  27230  clwlksfclwwlkOLD  27237  conngrv2edg  27368  frgrusgrfrcond  27434  3cyclfrgrrn1  27460  l2p  27663  strlem1  29439  vtocl2d  29644  ssiun2sf  29706  bnj981  31348  bnj1148  31392  consym1  32746  axc11n11  33000  bj-hbaeb2  33133  bj-restb  33371  bj-ismoored0  33385  clmgmOLD  33981  smgrpmgm  33994  smgrpassOLD  33995  grpomndo  34005  aecom-o  34708  hbae-o  34710  hbequid  34716  equidqe  34729  equid1ALT  34732  axc11nfromc11  34733  ax12inda  34755  zindbi  38031  exlimexi  39250  eexinst11  39253  e222  39381  e111  39419  e333  39480  stoweidlem34  40772  stoweidlem43  40781  funressnfv  41732  funbrafv  41762  ndmaovass  41810  ssfz12  41852  oexpnegALTV  42116  oexpnegnz  42117  mgm2mgm  42391
  Copyright terms: Public domain W3C validator