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  6384  tfr1onlemsucaccv  6400  tfrcllemsucaccv  6413  phplem3  6916  ssfilem  6937  diffitest  6949  reapmul1  8624  apsqgt0  8630  recexaplem2  8681  nnnn0addcl  9281  un0addcl  9284  un0mulcl  9285  elz2  9399  xrltso  9873  xaddnemnf  9934  xaddnepnf  9935  fzsplit2  10127  fzsuc2  10156  elfzp12  10176  seqf1oglem2  10614  expp1  10640  expnegap0  10641  expcllem  10644  mulexpzap  10673  expaddzap  10677  expmulzap  10679  zzlesq  10802  bcpasc  10860  xrltmaxsup  11424  xrmaxaddlem  11427  summodc  11550  fsumsplit  11574  fprodsplitdc  11763  ef0lem  11827  odd2np1  12040  dvdslcm  12247  lcmeq0  12249  lcmcl  12250  lcmneg  12252  lcmgcd  12256  rpexp1i  12332  pcid  12503  4sqlem16  12585  xpsfeq  12998  mulgneg  13280  mulgnn0z  13289  lgsdir2lem4  15282  lgsdir2  15284  lgsdirnn0  15298  lgsdinn0  15299