Theorem pm2.61d2 135

Description: Inference eliminating an antecedent.

Hypotheses

Ref	Expression
pm2.61d2.1	|- (ph -> (-. ps -> ch))
pm2.61d2.2	|- (ps -> ch)

Assertion

Ref	Expression
pm2.61d2	|- (ph -> ch)

Proof of Theorem pm2.61d2

Step	Hyp	Ref	Expression
1		pm2.61d2.2	. . 3 |- (ps -> ch)
2	1	a1i 8	. 2 |- (ph -> (ps -> ch))
3		pm2.61d2.1	. 2 |- (ph -> (-. ps -> ch))
4	2, 3	pm2.61d 133	1 |- (ph -> ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61ii 136  pm5.21nd 692  hbabd 1514  tfinds 3218  relimasn 3482  ndmoprcl 4102  curry1val 4158  f1oen2g 4455  f1domg 4457  fiint 4620  axpowndlem3 5016  ltapr 5216  xrmax1 5969  xrmin2 5972  max1ALT 5976  efseq1ex 7396  infxpidmlem8 7651  mdsymlem6 10419  sumdmdlem2 10430  clsrebb 10587  efilcp 10664  efilcp2 10669

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

Copyright terms: Public domain