Theorem pm2.61d2 143

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61ii 144  pm5.21nd 744  hbabd 1876  tfinds 3942  tfindsOLD 3943  relimasn 4288  ndmoprcl 4977  curry1val 5077  curry2val 5080  onfununi 5116  f1oen2g 5453  f1domg 5455  riotaprc 5567  fiint 5650  axpowndlem3 6103  ltapr 6303  xrmax1 7092  xrmin2 7095  max1ALT 7099  efseq1ex 8568  infxpidmlem8 8828  fixp 10180  mdsymlem6 11980  sumdmdlem2 11991  clsrebb 14844  efilcp 14922  efilcp2 14926  fnejoin1 15530  fbasfip 15556

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

Copyright terms: Public domain