Theorem jaoian 956

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

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 846

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 398  df-or 847

This theorem is referenced by:  ccase  1037  preq12nebg  4864  opthprneg  4866  elpreqpr  4868  tpres  7202  xaddnemnf  13215  xaddnepnf  13216  faclbnd  14250  faclbnd3  14252  faclbnd4lem1  14253  znf1o  21107  degltlem1  25590  ipasslem3  30117  padct  31975  fz1nntr  32046  xrge0iifhom  32948  bj-ideqg1ALT  36094  nn0addcom  41371  nn0mulcom  41375  fzsplit1nn0  41540  f1mo  47567