Theorem jaodan 786

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  787  ordi  805  andi  807  dcor  919  ccase  948  mpjao3dan  1285  relop  4684  poltletr  4934  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  phplem3  6741  ssfilem  6762  diffitest  6774  reapmul1  8350  apsqgt0  8356  recexaplem2  8406  nnnn0addcl  9000  un0addcl  9003  un0mulcl  9004  elz2  9115  xrltso  9575  xaddnemnf  9633  xaddnepnf  9634  fzsplit2  9823  fzsuc2  9852  elfzp12  9872  expp1  10293  expnegap0  10294  expcllem  10297  mulexpzap  10326  expaddzap  10330  expmulzap  10332  bcpasc  10505  xrltmaxsup  11019  xrmaxaddlem  11022  summodc  11145  fsumsplit  11169  ef0lem  11355  odd2np1  11559  dvdslcm  11739  lcmeq0  11741  lcmcl  11742  lcmneg  11744  lcmgcd  11748  rpexp1i  11821