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  125  impbid  203  ibi  258  anidms  558  3imp3i2anOLD  1446  tbw-bijust  1778  tbw-negdf  1779  equid  2108  nf5di  2294  nfdiOLD  2399  hbae  2479  vtoclgaf  3464  vtocl2gaf  3466  vtocl3gaf  3468  vtocl4ga  3471  elinti  4678  copsexg  5145  vtoclr  5364  ssrelrn  5516  idrefOLD  5720  relresfld  5876  tz7.7  5962  elfvmptrab1  6526  tfisi  7288  bropopvvv  7489  f1o2ndf1  7519  suppimacnv  7540  brovex  7583  tfrlem9  7717  tfrlem11  7720  odi  7896  nndi  7940  sbth  8319  sdomdif  8347  zorn2lem7  9609  alephexp2  9688  addcanpi  10006  mulcanpi  10007  indpi  10014  prcdnq  10100  reclem2pr  10155  lediv2a  11202  nn01to3  12000  fi1uzind  13496  cshwlen  13769  cshwidxmodr  13774  rlimres  14512  ndvdssub  15352  bitsinv1  15383  nn0seqcvgd  15502  modprm0  15727  setsstruct  16109  initoeu2  16870  symgfixelsi  18056  symgfixfo  18060  uvcendim  20396  slesolex  20700  pm2mpf1  20817  mp2pm2mplem4  20827  fiinopn  20919  jensenlem2  24928  umgrupgr  26212  uspgrushgr  26285  uspgrupgr  26286  usgruspgr  26288  usgredg2vlem2  26333  cplgrop  26561  lfgrwlkprop  26812  2pthnloop  26855  usgr2pthlem  26887  elwwlks2  27108  clwlkclwwlklem2fv2  27139  eleclclwwlkn  27227  hashecclwwlkn1  27228  umgrhashecclwwlk  27229  clwlksfclwwlkOLD  27236  conngrv2edg  27368  frgrusgrfrcond  27434  3cyclfrgrrn1  27460  l2p  27662  strlem1  29437  vtocl2d  29642  ssiun2sf  29703  bnj981  31343  bnj1148  31387  consym1  32736  axc11n11  32987  bj-hbaeb2  33118  bj-restb  33358  bj-ismoored0  33372  clmgmOLD  33961  smgrpmgm  33974  smgrpassOLD  33975  grpomndo  33985  aecom-o  34680  hbae-o  34682  hbequid  34688  equidqe  34701  equid1ALT  34704  axc11nfromc11  34705  ax12inda  34727  zindbi  38012  exlimexi  39228  eexinst11  39231  e222  39359  e111  39397  e333  39457  stoweidlem34  40730  stoweidlem43  40739  funressnfv  41662  funbrafv  41747  ndmaovass  41795  tz6.12i-afv2  41832  dfatcolem  41844  ssfz12  41899  oexpnegnz  42164  mgm2mgm  42431
  Copyright terms: Public domain W3C validator