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 50
Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 54. (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  63  pm2.18  121  impbid  201  ibi  255  anidms  675  3imp3i2an  1270  tbw-bijust  1614  tbw-negdf  1615  equid  1926  nf5di  2105  nfdiOLD  2213  hbae  2303  vtoclgaf  3244  vtocl2gaf  3246  vtocl3gaf  3248  vtocl4ga  3251  elinti  4415  copsexg  4876  vtoclr  5076  issref  5415  relresfld  5565  tz7.7  5652  elfvmptrab1  6198  tfisi  6928  bropopvvv  7120  f1o2ndf1  7150  suppimacnv  7171  brovex  7213  tfrlem9  7346  tfrlem11  7349  odi  7524  nndi  7568  sbth  7943  sdomdif  7971  zorn2lem7  9185  alephexp2  9260  addcanpi  9578  mulcanpi  9579  indpi  9586  prcdnq  9672  reclem2pr  9727  lediv2a  10769  nn01to3  11616  fi1uzind  13083  fi1uzindOLD  13089  cshwlen  13345  cshwidxmodr  13350  rlimres  14086  ndvdssub  14920  bitsinv1  14951  nn0seqcvgd  15070  modprm0  15297  initoeu2  16438  symgfixelsi  17627  symgfixfo  17631  uvcendim  19953  slesolex  20255  pm2mpf1  20371  mp2pm2mplem4  20381  fiinopn  20479  jensenlem2  24459  usgraidx2vlem2  25715  wlkcompim  25848  wlkdvspthlem  25931  usgra2adedgspthlem2  25934  clwlkcompim  26086  clwwlknprop  26094  clwlkisclwwlklem2fv2  26105  eleclclwwlkn  26154  hashecclwwlkn1  26155  usghashecclwwlk  26156  clwlkfclwwlk  26165  el2wlkonot  26190  2wlkonot3v  26196  2spthonot3v  26197  3cyclfrgrarn1  26333  3cyclfrgrarn  26334  extwwlkfablem2  26399  numclwlk1lem2foa  26412  frgrareg  26438  strlem1  28287  vtocl2d  28493  ssiun2sf  28554  bnj981  30068  bnj1148  30112  consym1  31383  axc11n11  31653  bj-hbaeb2  31787  bj-restb  32022  clmgmOLD  32614  smgrpmgm  32627  smgrpassOLD  32628  grpomndo  32638  aecom-o  32998  hbae-o  33000  hbequid  33006  equidqe  33019  equid1ALT  33022  axc11nfromc11  33023  ax12inda  33045  zindbi  36323  exlimexi  37545  eexinst11  37548  e222  37676  e111  37714  e333  37775  stoweidlem34  38721  stoweidlem43  38730  funressnfv  39651  funbrafv  39682  ndmaovass  39730  oexpnegALTV  39921  oexpnegnz  39922  ssrelrn  40126  ssfz12  40168  umgrupgr  40320  uspgrushgr  40397  uspgrupgr  40398  usgruspgr  40400  usgredg2vlem2  40445  cplgrop  40651  lfgrwlkprop  40888  2pthnloop  40929  usgr2pthlem  40961  uspgrn2crct  41003  elwwlks2  41162  clwlkclwwlklem2fv2  41197  eleclclwwlksn  41252  hashecclwwlksn1  41253  umgrhashecclwwlk  41254  clwlksfclwwlk  41261  conngrv2edg  41354  frgrusgrfrcond  41423  3cyclfrgrrn1  41447  av-numclwlk1lem2foa  41513  mgm2mgm  41645
  Copyright terms: Public domain W3C validator