Theorem jaoian 958

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 857	. 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒))
6	5	imp 406	1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  ccase  1037  preq12nebg  4819  opthprneg  4821  elpreqpr  4823  tpres  7147  xaddnemnf  13151  xaddnepnf  13152  faclbnd  14213  faclbnd3  14215  faclbnd4lem1  14216  znf1o  21506  degltlem1  26033  ipasslem3  30908  padct  32797  fz1nntr  32882  xrge0iifhom  34094  bj-ideqg1ALT  37370  nn0addcom  42717  nn0mulcom  42721  fzsplit1nn0  42996  f1mo  49098