Theorem jaodan 804

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 724	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 124	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  805  ordi  823  andi  825  dcor  943  ccase  972  mpjao3dan  1343  relop  4880  poltletr  5137  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  phplem3  7040  ssfilem  7062  ssfilemd  7064  diffitest  7076  pr1or2  7399  reapmul1  8775  apsqgt0  8781  recexaplem2  8832  nnnn0addcl  9432  un0addcl  9435  un0mulcl  9436  elz2  9551  xrltso  10031  xaddnemnf  10092  xaddnepnf  10093  fzsplit2  10285  fzsuc2  10314  elfzp12  10334  seqf1oglem2  10783  expp1  10809  expnegap0  10810  expcllem  10813  mulexpzap  10842  expaddzap  10846  expmulzap  10848  zzlesq  10971  bcpasc  11029  ccatass  11189  ccatrn  11190  ccatswrd  11255  ccatpfx  11286  cats1un  11306  xrltmaxsup  11822  xrmaxaddlem  11825  summodc  11949  fsumsplit  11973  fprodsplitdc  12162  ef0lem  12226  odd2np1  12439  dvdslcm  12646  lcmeq0  12648  lcmcl  12649  lcmneg  12651  lcmgcd  12655  rpexp1i  12731  pcid  12902  4sqlem16  12984  xpsfeq  13433  mulgneg  13732  mulgnn0z  13741  lgsdir2lem4  15766  lgsdir2  15768  lgsdirnn0  15782  lgsdinn0  15783