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  4816  poltletr  5070  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  phplem3  6915  ssfilem  6936  diffitest  6948  reapmul1  8622  apsqgt0  8628  recexaplem2  8679  nnnn0addcl  9279  un0addcl  9282  un0mulcl  9283  elz2  9397  xrltso  9871  xaddnemnf  9932  xaddnepnf  9933  fzsplit2  10125  fzsuc2  10154  elfzp12  10174  seqf1oglem2  10612  expp1  10638  expnegap0  10639  expcllem  10642  mulexpzap  10671  expaddzap  10675  expmulzap  10677  zzlesq  10800  bcpasc  10858  xrltmaxsup  11422  xrmaxaddlem  11425  summodc  11548  fsumsplit  11572  fprodsplitdc  11761  ef0lem  11825  odd2np1  12038  dvdslcm  12237  lcmeq0  12239  lcmcl  12240  lcmneg  12242  lcmgcd  12246  rpexp1i  12322  pcid  12493  4sqlem16  12575  xpsfeq  12988  mulgneg  13270  mulgnn0z  13279  lgsdir2lem4  15272  lgsdir2  15274  lgsdirnn0  15288  lgsdinn0  15289