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 494  ibi 590  3anidm12 878  equid 1113  alequcom 1125  hbae 1128  hbequid 1152  equid1 1253  ax11inda 1348  vtoclgaf 1826  sbcth2 1953  ssiun2s 2562  copsexg 2759  reuuni2f 2846  tz7.7 2936  nsuceq0 3016  tfrlem9 3858  tfrlem11 3860  oprabvalig 3963  omcl 4109  oecl 4110  odi 4148  nnmcl 4168  nnecl 4169  sbth 4391  zorn2lem6 4717  zorn2lem7 4718  mulcanpi 4950  indpi 4957  prcdpq 5020  ltaddpr 5063  reclem2pr 5080  reclem3pr 5081  lemulge11t 5755  lediv2it 5796  nn1suc 5838  ser1add2 6226  ser1add 6227  2climnn 6990  2climnn0 6991  infcvgaux2 7106  alephexp2 7479  ompfl2 8687  uninqs 8701  infi1 8706  fiiu 8709  ficli 8727  fiiu2 8734  bsi 8739  hmphre 8768  hmeogrp 8776  fillsb 8785  filint 8787  fipfil2 8789  filintf 8793  filint2 8796  iintlem1 8826  strlem1 10301

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

Copyright terms: Public domain