Theorem jaodan 809

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4930  poltletr  5188  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  phplem3  7155  ssfilem  7177  ssfilemd  7179  diffitest  7191  pr1or2  7540  reapmul1  8923  apsqgt0  8929  recexaplem2  8980  nnnn0addcl  9593  un0addcl  9596  un0mulcl  9597  elz2  9716  xrltso  10198  xaddnemnf  10259  xaddnepnf  10260  fzsplit2  10455  fzsplit3  10458  fzsuc2  10486  elfzp12  10506  seqf1oglem2  10957  expp1  10983  expnegap0  10984  expcllem  10987  mulexpzap  11016  expaddzap  11020  expmulzap  11022  zzlesq  11146  bcpasc  11204  ccatass  11376  ccatrn  11377  ccatswrd  11442  ccatpfx  11473  cats1un  11493  xrltmaxsup  12023  xrmaxaddlem  12026  summodc  12150  fsumsplit  12174  fprodsplitdc  12363  ef0lem  12427  odd2np1  12640  dvdslcm  12847  lcmeq0  12849  lcmcl  12850  lcmneg  12852  lcmgcd  12856  rpexp1i  12932  pcid  13103  4sqlem16  13185  xpsfeq  13666  mulgneg  13943  mulgnn0z  13952  lgsdir2lem4  16150  lgsdir2  16152  lgsdirnn0  16166  lgsdinn0  16167