Theorem jaoian 954

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 844

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 397  df-or 845

This theorem is referenced by:  ccase  1035  preq12nebg  4793  opthprneg  4795  elpreqpr  4797  tpres  7076  xaddnemnf  12970  xaddnepnf  12971  faclbnd  14004  faclbnd3  14006  faclbnd4lem1  14007  znf1o  20759  degltlem1  25237  ipasslem3  29195  padct  31054  fz1nntr  31125  xrge0iifhom  31887  bj-ideqg1ALT  35336  fzsplit1nn0  40576  f1mo  46180