Theorem pm2.61d2 129

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 127	1 |- (ph -> ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61ii 130  pm5.21nd 679  hbabd 1467  tfinds 3157  relimasn 3421  ndmoprcl 4039  curry1val 4093  f1oen2g 4384  f1domg 4386  fiint 4543  axpowndlem3 4934  ltapr 5134  xrmax1 5867  xrmin2 5870  max1ALT 5874  efseq1ex 7265  infxpidmlem8 7519  mdsymlem6 10291  sumdmdlem2 10302  clsrebb 10439  efilcp 10504  efilcp2 10509

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

Copyright terms: Public domain