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 680  hbabd 1468  tfinds 3161  relimasn 3425  ndmoprcl 4044  curry1val 4100  f1oen2g 4394  f1domg 4396  fiint 4559  fiintOLD 4560  axpowndlem3 4951  ltapr 5151  xrmax1 5909  xrmin2 5912  max1ALT 5916  efseq1ex 7306  infxpidmlem8 7559  mdsymlem6 10335  sumdmdlem2 10346  clsrebb 10493  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582

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

Copyright terms: Public domain