Theorem pm2.61ian 534

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 402	. 2 |- (ph -> (ps -> ch))
3		pm2.61ian.2	. . 3 |- ((-. ph /\ ps) -> ch)
4	3	ex 402	. 2 |- (-. ph -> (ps -> ch))
5	2, 4	pm2.61i 140	1 |- (ps -> ch)

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

This theorem is referenced by:  4cases 832  sbcom 1632  ax11indalem 1759  ifboth 3002  tfindsg 3944  findsg 3980  xpcan2 4350  funopg 4454  mapsspw 5400  ranklim 5796  climcl 8238  dscmet 9196  unopbd 11577  nmopcoi 11665  frsucopabn 13911  iintlem1 15010

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 164  df-an 242

Copyright terms: Public domain