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  877  ccase  906  mpjao3dan  1239  relop  4514  poltletr  4755  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  phplem3  6389  ssfilem  6410  diffitest  6421  reapmul1  7762  apsqgt0  7768  recexaplem2  7809  nnnn0addcl  8385  un0addcl  8388  un0mulcl  8389  elz2  8500  xrltso  8947  fzsplit2  9145  fzsuc2  9172  elfzp12  9192  expp1  9580  expnegap0  9581  expcllem  9584  mulexpzap  9613  expaddzap  9617  expmulzap  9619  bcpasc  9790  odd2np1  10417  dvdslcm  10595  lcmeq0  10597  lcmcl  10598  lcmneg  10600  lcmgcd  10604  rpexp1i  10677