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 1869  ra4sbc 1995  elinti 2539  trel 2684  trss 2686  elpwunsn 2909  onfr 2983  ordsucss 3066  limom 3143  vtoclr 3208  ralxp 3215  fvelima 3761  funfvima 3849  ensymg 4405  domsdomtr 4469  unifi 4545  fodomfi 4553  ltaprlem 5137  nnmulclt 5903  crulem 6687  chlim 9092  atcvatlem 10303  infi 10542

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

Copyright terms: Public domain