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

Step	Hyp	Ref	Expression
1		pm2.43i.1	. 2 |- (ph -> (ph -> ps))
2		pm2.43 63	. 2 |- ((ph -> (ph -> ps)) -> (ph -> ps))
3	1, 2	ax-mp 7	1 |- (ph -> ps)

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.18 81  anidm 432  anidms 434  anabsi5 495  ibi 592  3anidm12 882  ax4 972  equid 1126  ax10 1141  hbae 1145  equid1 1269  ax11inda 1371  vtoclgaf 1851  sbcth2 1982  ssiun2s 2594  copsexg 2792  reuuni2f 2883  tz7.7 2973  nsuceq0 3053  tfrlem9 3919  tfrlem11 3921  oprabvalig 4024  omcl 4171  oecl 4172  odi 4210  nnmcl 4230  nnecl 4231  sbth 4457  zorn2lem6 4793  zorn2lem7 4794  mulcanpi 5027  indpi 5034  prcdpq 5097  ltaddpr 5140  reclem2pr 5157  reclem3pr 5158  lediv2it 5897  nn1suc 5939  ser1add2 6338  ser1add 6339  2climnn 7102  2climnn0 7103  infcvgaux2 7220  alephexp2 7586  strlem1 10177  uninqs 10441  infi1 10447  infi1OLD 10448  fiiu 10453  fiiuOLD 10454  ficli 10472  ficliOLD 10473  fiiu2 10488  fiiu2OLD 10489  bsi 10495  hmphre 10530  hmeogrp 10538  homcard 10539  set2elt 10545  top2ind 10548  fillsb 10560  filint 10562  fipfil2 10564  fipfil2OLD 10565  filintf 10569  filint2 10574  filint2OLD 10575  iintlem1 10632  idfisf 10760

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

Copyright terms: Public domain