Theorem jaodan 744

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

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

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 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjaodan  745  ordi  763  andi  765  dcor  879  ccase  908  mpjao3dan  1241  relop  4554  poltletr  4799  tfrlemisucaccv  6044  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  phplem3  6522  ssfilem  6543  diffitest  6555  reapmul1  8013  apsqgt0  8019  recexaplem2  8060  nnnn0addcl  8636  un0addcl  8639  un0mulcl  8640  elz2  8751  xrltso  9198  fzsplit2  9396  fzsuc2  9423  elfzp12  9443  expp1  9860  expnegap0  9861  expcllem  9864  mulexpzap  9893  expaddzap  9897  expmulzap  9899  bcpasc  10070  isummo  10662  odd2np1  10748  dvdslcm  10926  lcmeq0  10928  lcmcl  10929  lcmneg  10931  lcmgcd  10935  rpexp1i  11008