Theorem jaodan 804

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  805  ordi  823  andi  825  dcor  943  ccase  972  mpjao3dan  1343  relop  4880  poltletr  5137  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  phplem3  7039  ssfilem  7061  ssfilemd  7063  diffitest  7075  pr1or2  7398  reapmul1  8774  apsqgt0  8780  recexaplem2  8831  nnnn0addcl  9431  un0addcl  9434  un0mulcl  9435  elz2  9550  xrltso  10030  xaddnemnf  10091  xaddnepnf  10092  fzsplit2  10284  fzsuc2  10313  elfzp12  10333  seqf1oglem2  10781  expp1  10807  expnegap0  10808  expcllem  10811  mulexpzap  10840  expaddzap  10844  expmulzap  10846  zzlesq  10969  bcpasc  11027  ccatass  11184  ccatrn  11185  ccatswrd  11250  ccatpfx  11281  cats1un  11301  xrltmaxsup  11817  xrmaxaddlem  11820  summodc  11943  fsumsplit  11967  fprodsplitdc  12156  ef0lem  12220  odd2np1  12433  dvdslcm  12640  lcmeq0  12642  lcmcl  12643  lcmneg  12645  lcmgcd  12649  rpexp1i  12725  pcid  12896  4sqlem16  12978  xpsfeq  13427  mulgneg  13726  mulgnn0z  13735  lgsdir2lem4  15759  lgsdir2  15761  lgsdirnn0  15775  lgsdinn0  15776