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 3271  phplem3 4499  ssnn 4523  1re 5418  lecase 5605  recextlem2 5666  xrsupsslem 6033  xrinfmsslem 6034  xrsupss 6035  xrinfmss 6036  flhalft 6201  expcllem 6520  expge1t 6538  exple1t 6552  cvg3 6875  faclbnd4lem3 6902  faclbnd4lem4 6903  faclbnd4 6904  fsumcmpndx2 6995  elcncf 7217  reeff1o 7385  ssblex 7818  lmsslem 7914  bcthlem16 7976  bcthlem20 7980  hmopidmchlem 10034

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