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  1318  relop  4795  poltletr  5047  tfrlemisucaccv  6349  tfr1onlemsucaccv  6365  tfrcllemsucaccv  6378  phplem3  6881  ssfilem  6902  diffitest  6914  reapmul1  8581  apsqgt0  8587  recexaplem2  8638  nnnn0addcl  9235  un0addcl  9238  un0mulcl  9239  elz2  9353  xrltso  9825  xaddnemnf  9886  xaddnepnf  9887  fzsplit2  10079  fzsuc2  10108  elfzp12  10128  expp1  10557  expnegap0  10558  expcllem  10561  mulexpzap  10590  expaddzap  10594  expmulzap  10596  zzlesq  10719  bcpasc  10777  xrltmaxsup  11296  xrmaxaddlem  11299  summodc  11422  fsumsplit  11446  fprodsplitdc  11635  ef0lem  11699  odd2np1  11909  dvdslcm  12100  lcmeq0  12102  lcmcl  12103  lcmneg  12105  lcmgcd  12109  rpexp1i  12185  pcid  12355  4sqlem16  12437  xpsfeq  12818  mulgneg  13077  mulgnn0z  13086  lgsdir2lem4  14885  lgsdir2  14887  lgsdirnn0  14901  lgsdinn0  14902