Theorem jaodan 798

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  799  ordi  817  andi  819  dcor  937  ccase  966  mpjao3dan  1319  relop  4827  poltletr  5082  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  phplem3  6950  ssfilem  6971  diffitest  6983  reapmul1  8667  apsqgt0  8673  recexaplem2  8724  nnnn0addcl  9324  un0addcl  9327  un0mulcl  9328  elz2  9443  xrltso  9917  xaddnemnf  9978  xaddnepnf  9979  fzsplit2  10171  fzsuc2  10200  elfzp12  10220  seqf1oglem2  10663  expp1  10689  expnegap0  10690  expcllem  10693  mulexpzap  10722  expaddzap  10726  expmulzap  10728  zzlesq  10851  bcpasc  10909  ccatass  11062  ccatrn  11063  xrltmaxsup  11539  xrmaxaddlem  11542  summodc  11665  fsumsplit  11689  fprodsplitdc  11878  ef0lem  11942  odd2np1  12155  dvdslcm  12362  lcmeq0  12364  lcmcl  12365  lcmneg  12367  lcmgcd  12371  rpexp1i  12447  pcid  12618  4sqlem16  12700  xpsfeq  13148  mulgneg  13447  mulgnn0z  13456  lgsdir2lem4  15479  lgsdir2  15481  lgsdirnn0  15495  lgsdinn0  15496