Theorem pm2.43b 67

Description: Inference absorbing redundant antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem pm2.43b

Step	Hyp	Ref	Expression
1		pm2.43a.1	. . 3 |- (ps -> (ph -> (ps -> ch)))
2	1	pm2.43a 66	. 2 |- (ps -> (ph -> ch))
3	2	com12 11	1 |- (ph -> (ps -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  anabsi7 497  rcla4 1871  ra4sbc 1997  elinti 2542  trel 2687  trss 2689  elpwunsn 2912  onfr 2986  ordsucss 3069  limom 3146  vtoclr 3211  ralxp 3218  fvelima 3764  funfvima 3852  ensymg 4411  domsdomtr 4476  unifiOLD 4557  fodomfiOLD 4566  ltaprlem 5150  nnmulclt 5941  crulem 6736  chlim 9104  atcvatlem 10312  infi 10578  infiOLD 10579

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

Copyright terms: Public domain