Theorem jaodan 802

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 115	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 722	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 124	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  803  ordi  821  andi  823  dcor  941  ccase  970  mpjao3dan  1341  relop  4872  poltletr  5129  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  phplem3  7023  ssfilem  7045  diffitest  7057  pr1or2  7378  reapmul1  8753  apsqgt0  8759  recexaplem2  8810  nnnn0addcl  9410  un0addcl  9413  un0mulcl  9414  elz2  9529  xrltso  10004  xaddnemnf  10065  xaddnepnf  10066  fzsplit2  10258  fzsuc2  10287  elfzp12  10307  seqf1oglem2  10754  expp1  10780  expnegap0  10781  expcllem  10784  mulexpzap  10813  expaddzap  10817  expmulzap  10819  zzlesq  10942  bcpasc  11000  ccatass  11156  ccatrn  11157  ccatswrd  11217  ccatpfx  11248  cats1un  11268  xrltmaxsup  11783  xrmaxaddlem  11786  summodc  11909  fsumsplit  11933  fprodsplitdc  12122  ef0lem  12186  odd2np1  12399  dvdslcm  12606  lcmeq0  12608  lcmcl  12609  lcmneg  12611  lcmgcd  12615  rpexp1i  12691  pcid  12862  4sqlem16  12944  xpsfeq  13393  mulgneg  13692  mulgnn0z  13701  lgsdir2lem4  15725  lgsdir2  15727  lgsdirnn0  15741  lgsdinn0  15742