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 1630  opth2 2795  pw2en 4432  suppr 4570  pm2.61ltle 5515  xrmax2 5866  xrmin1 5867  xrsupsslem 6031  xrinfmsslem 6032  elioo3g 6325  elfz2t 6412  fzneuzt 6458  bcclt 6918  znnen 7453  metxp 7786  dscmet 7870  metelcls 7916  pstr 8594  nmcoplb 9896  nmophm 9899  nmbdfnlb 9916  nmcfnlb 9925

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