Theorem jaoian 957

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 848

This theorem is referenced by:  ccase  1038  preq12nebg  4773  opthprneg  4775  elpreqpr  4777  tpres  7016  xaddnemnf  12826  xaddnepnf  12827  faclbnd  13856  faclbnd3  13858  faclbnd4lem1  13859  znf1o  20516  degltlem1  24970  ipasslem3  28914  padct  30774  fz1nntr  30845  xrge0iifhom  31601  bj-ideqg1ALT  35071  fzsplit1nn0  40279  f1mo  45853