Theorem pm2.43a 60

Description: Inference absorbing redundant antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem pm2.43a

Step	Hyp	Ref	Expression
1		pm2.43a.1	. . 3 |- (ps -> (ph -> (ps -> ch)))
2	1	com23 32	. 2 |- (ps -> (ps -> (ph -> ch)))
3	2	pm2.43i 58	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 2

This theorem is referenced by:  pm2.43b 61  rax4 1471  intss1 1979  ordsucelsuc 2324  tfinds 2401  fneu 2728  tz6.12i 2847  fvopab3ig 2869  fvopab2 2878  nndi 3180  pssnn 3428  inf3lem2 3465  rankr1 3518  zornlem7 3609  prlem936b 3948  reclem3pr 3952  uzind 4603  chcmh 5148

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org