Theorem jaodan 426

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 371	. . 3 |- (ph -> (ps -> ch))
3		jaodan.2	. . . 4 |- ((ph /\ th) -> ch)
4	3	ex 371	. . 3 |- (ph -> (th -> ch))
5	2, 4	jaod 424	. 2 |- (ph -> ((ps \/ th) -> ch))
6	5	imp 348	1 |- ((ph /\ (ps \/ th)) -> ch)

Syntax hints:   -> wi 3   \/ wo 220   /\ wa 221

This theorem is referenced by:  relop 3365  oeoa 4360  oeoe 4362  phplem3 4657  ssnnfi 4682  1re 5589  lecasei 5775  recextlem2 5839  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  flhalf 6446  expcllem 6770  expne0i 6782  expge1 6787  exple1 6804  cvg3i 7126  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd4 7155  fsumcmpndx2 7245  elcncf 7470  reeff1o 7634  ssblex 8066  lmsslem 8163  bcthlem16 8225  bcthlem20 8229  abssinper 8980  hmopidmchlem 10358  divexp 11859  sdc 11877  incsequz2 11880  fsumlt1 11894  geomcau 11914  piececn 11955  phtpycolem2 12094  phtpycolem5 12097  phtpyco 12098

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 145  df-or 222  df-an 223

Copyright terms: Public domain