Theorem jaodan 805

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  806  ordi  824  andi  826  dcor  944  ccase  973  mpjao3dan  1344  relop  4886  poltletr  5144  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  phplem3  7083  ssfilem  7105  ssfilemd  7107  diffitest  7119  pr1or2  7442  reapmul1  8817  apsqgt0  8823  recexaplem2  8874  nnnn0addcl  9474  un0addcl  9477  un0mulcl  9478  elz2  9595  xrltso  10075  xaddnemnf  10136  xaddnepnf  10137  fzsplit2  10330  fzsuc2  10359  elfzp12  10379  seqf1oglem2  10828  expp1  10854  expnegap0  10855  expcllem  10858  mulexpzap  10887  expaddzap  10891  expmulzap  10893  zzlesq  11016  bcpasc  11074  ccatass  11234  ccatrn  11235  ccatswrd  11300  ccatpfx  11331  cats1un  11351  xrltmaxsup  11880  xrmaxaddlem  11883  summodc  12007  fsumsplit  12031  fprodsplitdc  12220  ef0lem  12284  odd2np1  12497  dvdslcm  12704  lcmeq0  12706  lcmcl  12707  lcmneg  12709  lcmgcd  12713  rpexp1i  12789  pcid  12960  4sqlem16  13042  xpsfeq  13491  mulgneg  13790  mulgnn0z  13799  lgsdir2lem4  15833  lgsdir2  15835  lgsdirnn0  15849  lgsdinn0  15850