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  678  3imp3i2anOLD  1300  tbw-bijust  1663  tbw-negdf  1664  equid  1985  nf5di  2157  nfdiOLD  2261  hbae  2348  vtoclgaf  3302  vtocl2gaf  3304  vtocl3gaf  3306  vtocl4ga  3309  elinti  4517  copsexg  4985  vtoclr  5198  ssrelrn  5347  issref  5544  relresfld  5700  tz7.7  5787  elfvmptrab1  6344  tfisi  7100  bropopvvv  7300  f1o2ndf1  7330  suppimacnv  7351  brovex  7393  tfrlem9  7526  tfrlem11  7529  odi  7704  nndi  7748  sbth  8121  sdomdif  8149  zorn2lem7  9362  alephexp2  9441  addcanpi  9759  mulcanpi  9760  indpi  9767  prcdnq  9853  reclem2pr  9908  lediv2a  10955  nn01to3  11819  fi1uzind  13317  cshwlen  13591  cshwidxmodr  13596  rlimres  14333  ndvdssub  15180  bitsinv1  15211  nn0seqcvgd  15330  modprm0  15557  setsstruct  15945  initoeu2  16713  symgfixelsi  17901  symgfixfo  17905  uvcendim  20234  slesolex  20536  pm2mpf1  20652  mp2pm2mplem4  20662  fiinopn  20754  jensenlem2  24759  umgrupgr  26043  uspgrushgr  26115  uspgrupgr  26116  usgruspgr  26118  usgredg2vlem2  26163  cplgrop  26389  lfgrwlkprop  26640  2pthnloop  26683  usgr2pthlem  26715  elwwlks2  26933  clwlkclwwlklem2fv2  26962  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  conngrv2edg  27173  frgrusgrfrcond  27239  3cyclfrgrrn1  27265  l2p  27461  strlem1  29237  vtocl2d  29442  ssiun2sf  29504  bnj981  31146  bnj1148  31190  consym1  32544  axc11n11  32797  bj-hbaeb2  32930  bj-restb  33172  bj-ismoored0  33186  clmgmOLD  33780  smgrpmgm  33793  smgrpassOLD  33794  grpomndo  33804  aecom-o  34505  hbae-o  34507  hbequid  34513  equidqe  34526  equid1ALT  34529  axc11nfromc11  34530  ax12inda  34552  zindbi  37828  exlimexi  39047  eexinst11  39050  e222  39178  e111  39216  e333  39277  stoweidlem34  40569  stoweidlem43  40578  funressnfv  41529  funbrafv  41559  ndmaovass  41607  ssfz12  41649  oexpnegALTV  41913  oexpnegnz  41914  mgm2mgm  42188
 Copyright terms: Public domain W3C validator