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

Syntax hints:   -> wi 3   \/ wo 222   /\ wa 223

This theorem is referenced by:  relop 3275  phplem3 4510  ssnnfi 4535  ssnnfiOLD 4536  1re 5435  lecase 5621  recextlem2 5683  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  flhalft 6246  expcllem 6575  expge1t 6593  exple1t 6607  cvg3 6923  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd4 6952  fsumcmpndx2 7042  elcncf 7265  reeff1o 7426  ssblex 7856  lmsslem 7952  bcthlem16 8014  bcthlem20 8018  sinkpi 8697  abssinper 8712  hmopidmchlem 10078

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-or 224  df-an 225

Copyright terms: Public domain