Theorem jaoian 971

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 417	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaoian.2	. . . 4 ⊢ ((𝜃 ∧ 𝜓) → 𝜒)
4	3	ex 417	. . 3 ⊢ (𝜃 → (𝜓 → 𝜒))
5	2, 4	jaoi 870	. 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒))
6	5	imp 411	1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  ccase  1051  preq12nebg  4829  opthprneg  4831  elpreqpr  4833  tpres  7197  xaddnemnf  13258  xaddnepnf  13259  faclbnd  14322  faclbnd3  14324  faclbnd4lem1  14325  znf1o  21666  degltlem1  26194  ipasslem3  31122  padct  33000  fz1nntr  33084  xrge0iifhom  34268  bj-ideqg1ALT  37692  nn0addcom  43121  nn0mulcom  43125  fzsplit1nn0  43372  f1mo  49511