Theorem jaodan 787

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

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

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  788  ordi  806  andi  808  dcor  920  ccase  949  mpjao3dan  1289  relop  4733  poltletr  4983  tfrlemisucaccv  6266  tfr1onlemsucaccv  6282  tfrcllemsucaccv  6295  phplem3  6792  ssfilem  6813  diffitest  6825  reapmul1  8453  apsqgt0  8459  recexaplem2  8509  nnnn0addcl  9103  un0addcl  9106  un0mulcl  9107  elz2  9218  xrltso  9685  xaddnemnf  9743  xaddnepnf  9744  fzsplit2  9934  fzsuc2  9963  elfzp12  9983  expp1  10408  expnegap0  10409  expcllem  10412  mulexpzap  10441  expaddzap  10445  expmulzap  10447  bcpasc  10622  xrltmaxsup  11136  xrmaxaddlem  11139  summodc  11262  fsumsplit  11286  fprodsplitdc  11475  ef0lem  11539  odd2np1  11745  dvdslcm  11926  lcmeq0  11928  lcmcl  11929  lcmneg  11931  lcmgcd  11935  rpexp1i  12008