Theorem pm2.43i 64

Description: Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.)

Hypothesis

Ref	Expression
pm2.43i.1	|- (ph -> (ph -> ps))

Assertion

Ref	Expression
pm2.43i	|- (ph -> ps)

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2		pm2.43i.1	. 2 |- (ph -> (ph -> ps))
3	1, 2	mpd 26	1 |- (ph -> ps)

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.18 84  anidm 442  anidms 444  anabsi5 506  ibi 603  3anidm12 894  ax4 1013  equid 1167  equidALT 1168  ax10 1183  hbae 1187  equid1 1311  ax11inda 1413  vtoclgaf 1898  sbcth2 2032  ssiun2s 2648  copsexg 2848  reuuni2f 2940  tz7.7 3030  nsuceq0 3110  tfrlem9 3977  tfrlem11 3979  oprabvalig 4082  omcl 4229  oecl 4230  odi 4268  nnmcl 4288  nnecl 4289  sbth 4520  zorn2lem6 4855  zorn2lem7 4856  mulcanpi 5092  indpi 5099  prcdpq 5162  ltaddpr 5205  reclem2pr 5222  reclem3pr 5223  lediv2a 5957  nn1suc 5999  ser1add2i 6597  ser1addi 6598  2climnni 7192  2climnn0i 7193  infcvgaux2i 7310  alephexp2 7678  strlem1 10261  uninqs 10527  infi1 10532  fiiu 10535  ficli 10553  ref3w 10566  fiiu2 10574  bsi 10589  hmphre 10624  hmeogrp 10632  homcard 10633  set2elt 10639  top2ind 10642  filint 10656  fipfil2 10658  filintf 10662  filint2 10665  iintlem1 10714  idfisf 10844

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain