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 678  hbabd 1461  tfinds 3151  relimasn 3409  ndmoprcl 4030  curry1val 4084  f1oen2g 4375  f1domg 4377  fiint 4534  axpowndlem3 4923  ltapr 5123  xrmax1 5857  xrmin2 5860  max1ALT 5864  efseq1ex 7248  infxpidmlem8 7502  mdsymlem6 10243  sumdmdlem2 10253  clsrebb 10380  efilcp 10445  efilcp2 10450

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

Copyright terms: Public domain