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.18OLD  129  impbid  215  anidms  570  tbw-bijust  1700  tbw-negdf  1701  equid  2020  nf5di  2295  hbae  2455  vtoclgaf  3558  vtoclga  3559  vtocl2gaf  3561  vtocl3gaf  3562  vtocl4ga  3565  vtocl2dOLD  3913  elinti  4866  copsexgw  5362  copsexg  5363  vtoclr  5596  ssrelrn  5744  relresfld  6108  tz7.7  6198  elfvmptrab1  6776  tfisi  7556  bropopvvv  7768  f1o2ndf1  7801  suppimacnv  7824  brovex  7871  tfrlem9  8004  tfrlem11  8007  odi  8188  nndi  8232  sbth  8621  sdomdif  8649  zorn2lem7  9909  alephexp2  9988  addcanpi  10306  mulcanpi  10307  indpi  10314  prcdnq  10400  reclem2pr  10455  lediv2a  11519  nn01to3  12327  fi1uzind  13849  cshwlen  14150  cshwidxmodr  14155  rlimres  14904  ndvdssub  15747  bitsinv1  15778  nn0seqcvgd  15901  modprm0  16129  setsstruct  16512  initoeu2  17265  symgfixelsi  18552  symgfixfo  18556  uvcendim  20977  slesolex  21277  pm2mpf1  21393  mp2pm2mplem4  21403  fiinopn  21495  jensenlem2  25562  umgrupgr  26885  uspgrushgr  26957  uspgrupgr  26958  usgruspgr  26960  usgredg2vlem2  27005  cplgrop  27216  lfgrwlkprop  27466  2pthnloop  27509  usgr2pthlem  27541  elwwlks2  27741  clwlkclwwlklem2fv2  27770  eleclclwwlkn  27850  hashecclwwlkn1  27851  umgrhashecclwwlk  27852  conngrv2edg  27969  3cyclfrgrrn1  28059  l2p  28251  strlem1  30022  ssiun2sf  30308  bnj981  32240  bnj1148  32286  swrdrevpfx  32381  consym1  33786  axc11n11  34034  bj-hbaeb2  34160  curryset  34285  currysetlem3  34288  bj-restb  34413  wl-axc11rc11  34880  clmgmOLD  35189  smgrpmgm  35202  smgrpassOLD  35203  grpomndo  35213  aecom-o  36097  hbae-o  36099  hbequid  36105  equidqe  36118  equid1ALT  36121  axc11nfromc11  36122  ax12inda  36144  zindbi  39719  exlimexi  41066  eexinst11  41069  e222  41178  e111  41216  e333  41275  stoweidlem34  42518  stoweidlem43  42527  funressnfv  43477  funbrafv  43556  ndmaovass  43604  tz6.12i-afv2  43641  dfatcolem  43653  ssfz12  43713  oexpnegnz  44038  fpprel2  44101  mgm2mgm  44329
 Copyright terms: Public domain W3C validator