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  4813  poltletr  5067  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  phplem3  6912  ssfilem  6933  diffitest  6945  reapmul1  8616  apsqgt0  8622  recexaplem2  8673  nnnn0addcl  9273  un0addcl  9276  un0mulcl  9277  elz2  9391  xrltso  9865  xaddnemnf  9926  xaddnepnf  9927  fzsplit2  10119  fzsuc2  10148  elfzp12  10168  seqf1oglem2  10594  expp1  10620  expnegap0  10621  expcllem  10624  mulexpzap  10653  expaddzap  10657  expmulzap  10659  zzlesq  10782  bcpasc  10840  xrltmaxsup  11403  xrmaxaddlem  11406  summodc  11529  fsumsplit  11553  fprodsplitdc  11742  ef0lem  11806  odd2np1  12017  dvdslcm  12210  lcmeq0  12212  lcmcl  12213  lcmneg  12215  lcmgcd  12219  rpexp1i  12295  pcid  12465  4sqlem16  12547  xpsfeq  12931  mulgneg  13213  mulgnn0z  13222  lgsdir2lem4  15188  lgsdir2  15190  lgsdirnn0  15204  lgsdinn0  15205