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  676  3imp3i2an  1275  tbw-bijust  1620  tbw-negdf  1621  equid  1936  nf5di  2116  nfdiOLD  2224  hbae  2314  vtoclgaf  3261  vtocl2gaf  3263  vtocl3gaf  3265  vtocl4ga  3268  elinti  4457  copsexg  4926  vtoclr  5134  ssrelrn  5285  issref  5478  relresfld  5631  tz7.7  5718  elfvmptrab1  6271  tfisi  7020  bropopvvv  7215  f1o2ndf1  7245  suppimacnv  7266  brovex  7308  tfrlem9  7441  tfrlem11  7444  odi  7619  nndi  7663  sbth  8040  sdomdif  8068  zorn2lem7  9284  alephexp2  9363  addcanpi  9681  mulcanpi  9682  indpi  9689  prcdnq  9775  reclem2pr  9830  lediv2a  10877  nn01to3  11741  fi1uzind  13234  fi1uzindOLD  13240  cshwlen  13498  cshwidxmodr  13503  rlimres  14239  ndvdssub  15076  bitsinv1  15107  nn0seqcvgd  15226  modprm0  15453  setsstruct  15838  initoeu2  16606  symgfixelsi  17795  symgfixfo  17799  uvcendim  20126  slesolex  20428  pm2mpf1  20544  mp2pm2mplem4  20554  fiinopn  20646  jensenlem2  24648  umgrupgr  25927  uspgrushgr  25997  uspgrupgr  25998  usgruspgr  26000  usgredg2vlem2  26045  cplgrop  26254  lfgrwlkprop  26487  2pthnloop  26530  usgr2pthlem  26562  elwwlks2  26762  clwlkclwwlklem2fv2  26798  eleclclwwlksn  26853  hashecclwwlksn1  26854  umgrhashecclwwlk  26855  clwlksfclwwlk  26862  conngrv2edg  26955  frgrusgrfrcond  27023  3cyclfrgrrn1  27047  numclwlk1lem2foa  27113  l2p  27219  strlem1  28997  vtocl2d  29203  ssiun2sf  29264  bnj981  30781  bnj1148  30825  consym1  32114  axc11n11  32367  bj-hbaeb2  32501  bj-restb  32737  clmgmOLD  33321  smgrpmgm  33334  smgrpassOLD  33335  grpomndo  33345  aecom-o  33705  hbae-o  33707  hbequid  33713  equidqe  33726  equid1ALT  33729  axc11nfromc11  33730  ax12inda  33752  zindbi  37030  exlimexi  38251  eexinst11  38254  e222  38382  e111  38420  e333  38481  stoweidlem34  39588  stoweidlem43  39597  funressnfv  40542  funbrafv  40572  ndmaovass  40620  ssfz12  40651  oexpnegALTV  40917  oexpnegnz  40918  mgm2mgm  41181
  Copyright terms: Public domain W3C validator