Theorem jaoian 953

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)

Hypotheses

Ref	Expression
jaoian.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaoian.2	⊢ ((𝜃 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
jaoian	⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)

Proof of Theorem jaoian

Step	Hyp	Ref	Expression
1		jaoian.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 415	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaoian.2	. . . 4 ⊢ ((𝜃 ∧ 𝜓) → 𝜒)
4	3	ex 415	. . 3 ⊢ (𝜃 → (𝜓 → 𝜒))
5	2, 4	jaoi 853	. 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒))
6	5	imp 409	1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844

This theorem is referenced by:  ccase  1032  preq12nebg  4786  opthprneg  4788  elpreqpr  4790  tpres  6957  xaddnemnf  12623  xaddnepnf  12624  faclbnd  13644  faclbnd3  13646  faclbnd4lem1  13647  znf1o  20692  degltlem1  24660  ipasslem3  28604  padct  30449  fz1nntr  30521  xrge0iifhom  31175  bj-ideqg1ALT  34451  fzsplit1nn0  39344