HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem pm2.43i 64
Description: Inference absorbing redundant antecedent.
Hypothesis
Ref Expression
pm2.43i.1 |- (ph -> (ph -> ps))
Assertion
Ref Expression
pm2.43i |- (ph -> ps)
Proof of Theorem pm2.43i
StepHypRef Expression
1 pm2.43i.1 . 2 |- (ph -> (ph -> ps))
2 pm2.43 63 . 2 |- ((ph -> (ph -> ps)) -> (ph -> ps))
31, 2ax-mp 7 1 |- (ph -> ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  pm2.18 81  anidm 432  anidms 434  anabsi5 494  ibi 590  3anidm12 879  ax4 969  equid 1122  ax10 1137  hbae 1141  hbequid 1165  equid1 1264  ax11inda 1364  vtoclgaf 1842  sbcth2 1972  ssiun2s 2584  copsexg 2782  reuuni2f 2873  tz7.7 2963  nsuceq0 3043  tfrlem9 3904  tfrlem11 3906  oprabvalig 4009  omcl 4155  oecl 4156  odi 4194  nnmcl 4214  nnecl 4215  sbth 4437  zorn2lem6 4765  zorn2lem7 4766  mulcanpi 4999  indpi 5006  prcdpq 5069  ltaddpr 5112  reclem2pr 5129  reclem3pr 5130  lemulge11t 5804  lediv2it 5845  nn1suc 5887  ser1add2 6275  ser1add 6276  2climnn 7039  2climnn0 7040  infcvgaux2 7155  alephexp2 7528  strlem1 10087  ompfl2OLD 10327  uninqs 10342  infi1 10347  fiiu 10350  ficli 10368  fiiu2 10377  bsi 10382  hmphre 10417  hmeogrp 10425  homcard 10426  fillsb 10435  filint 10437  fipfil2 10439  filintf 10443  filint2 10446  iintlem1 10476
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain