Theorem jaodan 471

Description: Deduction disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaodan.1	|- ((ph /\ ps) -> ch)
jaodan.2	|- ((ph /\ th) -> ch)

Assertion

Ref	Expression
jaodan	|- ((ph /\ (ps \/ th)) -> ch)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 402	. . 3 |- (ph -> (ps -> ch))
3		jaodan.2	. . . 4 |- ((ph /\ th) -> ch)
4	3	ex 402	. . 3 |- (ph -> (th -> ch))
5	2, 4	jaod 469	. 2 |- (ph -> ((ps \/ th) -> ch))
6	5	imp 377	1 |- ((ph /\ (ps \/ th)) -> ch)

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240

This theorem is referenced by:  relop 4113  oeoa 5272  oeoe 5274  phplem3 5604  ssnnfi 5629  1re 6598  lecasei 6804  recextlem2 6875  xrsupsslem 7285  xrinfmsslem 7286  xrsupss 7287  xrinfmss 7288  flhalf 7487  expcllem 7818  expne0i 7830  expge1 7835  exple1 7852  cvg3i 8175  faclbnd4lem3 8202  faclbnd4lem4 8203  faclbnd4 8204  fsumcmpndx2 8302  elcncf 8527  reeff1o 8691  ssblex 9133  lmsslem 9230  bcthlem16 9292  bcthlem20 9296  abssinper 10062  hmopidmchlem 11722  gcdcllem3 13720  axfelem15 14045  eqfnun 15705  zornn0 15764  divexp 15779  elfzp12 15795  sdc 15811  fdc 15812  incsequz2 15816  fsumlt1 15831  geomcau 15849  oprpiece1res2 15881  piececn 15894  phtpycolem2 16052  phtpycolem5 16055  phtpyco 16056  pcoval2 16075  pcocn 16076  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  unichnidl 16179  lubun 16899  lubunNEW 16900  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-or 241  df-an 242

Copyright terms: Public domain