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 755  sbcom 1242  ax11indalem 1345  ifboth 2346  findsg 3120  tfindsg 3125  mapsspw 4279  ranklim 4609  climcl 6867  dscmet 7804  iintlem1 8826  unopbdt 10069  nmopco 10156

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