Theorem pm2.61ian 475

Description: Elimination of an antecedent.

Hypotheses

Ref	Expression
pm2.61ian.1	|- ((ph /\ ps) -> ch)
pm2.61ian.2	|- ((-. ph /\ ps) -> ch)

Assertion

Ref	Expression
pm2.61ian	|- (ps -> ch)

Proof of Theorem pm2.61ian

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	ex 373	. 2 |- (ph -> (ps -> ch))
3		pm2.61ian.2	. . 3 |- ((-. ph /\ ps) -> ch)
4	3	ex 373	. 2 |- (-. ph -> (ps -> ch))
5	2, 4	pm2.61i 126	1 |- (ps -> ch)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223

This theorem is referenced by:  4cases 756  sbcom 1253  ax11indalem 1361  ifboth 2365  findsg 3147  tfindsg 3152  funopg 3533  mapsspw 4325  ranklim 4657  climcl 6916  dscmet 7856  unopbdt 9855  nmopco 9942  iintlem1 10476

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain