Theorem pm2.61dan 535

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

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

This theorem is referenced by:  pm2.61neOLD 2088  opth2 3546  xpcan 4348  oeoa 5272  oeoe 5274  pw2en 5505  riotabidva 5575  suppr 5680  pm2.61ltlei 6705  xrmax2 7093  xrmin1 7094  xrsupsslem 7285  xrinfmsslem 7286  elioo3g 7547  elfz2 7642  fzneuz 7697  bccl 8224  znnen 8771  metxp 9111  dscmet 9196  metelcls 9243  pstr 9995  nmcoplbi 11595  nmophmi 11598  nmbdfnlbi 11615  nmcfnlbi 11624  nn0seqcvgd 13659  gcddvds 13722  gcdcl 13724  gcd0id 13729  gcdneg 13732  eucalgf 13751  eucalginv 13752  eucalglt 13753  fvrn0 13837  trcllem1 13933  opnnei 15417  topmeet 15526  topjoin 15527  difxp 15690  ifeq1da 15693  ifeq2da 15694  ifclda 15695  fzfi2 15787  rrntotbnd 16022  paddasslem18 17298  pmodlem2 17308

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