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  30086  padct  31944  fz1nntr  32015  xrge0iifhom  32917  bj-ideqg1ALT  36046  nn0addcom  41323  nn0mulcom  41327  fzsplit1nn0  41492  f1mo  47519