Theorem pm2.61ian 476

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 758  sbcom 1258  ax11indalem 1368  ifboth 2375  findsg 3157  tfindsg 3162  funopg 3547  mapsspw 4341  ranklim 4685  climcl 6978  dscmet 7918  unopbdt 9940  nmopco 10028  iintlem1 10632

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