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

Syntax hints:   → wi 4   ∧ wa 395   ∨ 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 206  df-an 396  df-or 844

This theorem is referenced by:  ccase  1034  preq12nebg  4790  opthprneg  4792  elpreqpr  4794  tpres  7058  xaddnemnf  12899  xaddnepnf  12900  faclbnd  13932  faclbnd3  13934  faclbnd4lem1  13935  znf1o  20671  degltlem1  25142  ipasslem3  29096  padct  30956  fz1nntr  31027  xrge0iifhom  31789  bj-ideqg1ALT  35263  fzsplit1nn0  40492  f1mo  46068