Theorem jaodan 743

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 113	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 113	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 669	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 122	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjaodan  744  ordi  762  andi  764  dcor  876  ccase  905  mpjao3dan  1238  relop  4504  poltletr  4745  tfrlemisucaccv  5962  phplem3  6340  ssfilem  6360  diffitest  6371  reapmul1  7695  apsqgt0  7701  recexaplem2  7742  nnnn0addcl  8318  un0addcl  8321  un0mulcl  8322  elz2  8419  xrltso  8871  fzsplit2  9069  fzsuc2  9096  elfzp12  9116  expp1  9483  expnegap0  9484  expcllem  9487  mulexpzap  9516  expaddzap  9520  expmulzap  9522  bcpasc  9693  odd2np1  10272  dvdslcm  10451  lcmeq0  10453  lcmcl  10454  lcmneg  10456  lcmgcd  10460  rpexp1i  10533