Theorem pm2.61dan 477

Description: Elimination of an antecedent.

Hypotheses

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

Assertion

Ref	Expression
pm2.61dan	|- (ph -> ch)

Proof of Theorem pm2.61dan

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

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

This theorem is referenced by:  pm2.61ne 1633  opth2 2800  pw2en 4446  suppr 4590  pm2.61ltle 5534  xrmax2 5910  xrmin1 5911  xrsupsslem 6076  xrinfmsslem 6077  elioo3g 6380  elfz2t 6472  fzneuzt 6518  bcclt 6972  znnen 7502  metxp 7834  dscmet 7918  metelcls 7965  pstr 8652  nmcoplb 9958  nmophm 9961  nmbdfnlb 9978  nmcfnlb 9987

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