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  4817  poltletr  5071  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  phplem3  6924  ssfilem  6945  diffitest  6957  reapmul1  8641  apsqgt0  8647  recexaplem2  8698  nnnn0addcl  9298  un0addcl  9301  un0mulcl  9302  elz2  9416  xrltso  9890  xaddnemnf  9951  xaddnepnf  9952  fzsplit2  10144  fzsuc2  10173  elfzp12  10193  seqf1oglem2  10631  expp1  10657  expnegap0  10658  expcllem  10661  mulexpzap  10690  expaddzap  10694  expmulzap  10696  zzlesq  10819  bcpasc  10877  xrltmaxsup  11441  xrmaxaddlem  11444  summodc  11567  fsumsplit  11591  fprodsplitdc  11780  ef0lem  11844  odd2np1  12057  dvdslcm  12264  lcmeq0  12266  lcmcl  12267  lcmneg  12269  lcmgcd  12273  rpexp1i  12349  pcid  12520  4sqlem16  12602  xpsfeq  13049  mulgneg  13348  mulgnn0z  13357  lgsdir2lem4  15380  lgsdir2  15382  lgsdirnn0  15396  lgsdinn0  15397