Theorem jaoian 971

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

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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 401  df-or 861

This theorem is referenced by:  ccase  1053  preq12nebg  4828  opthprneg  4830  elpreqpr  4832  tpres  7199  xaddnemnf  13257  xaddnepnf  13258  faclbnd  14322  faclbnd3  14324  faclbnd4lem1  14325  znf1o  21701  degltlem1  26229  ipasslem3  31185  padct  33063  fz1nntr  33147  xrge0iifhom  34327  bj-ideqg1ALT  37809  nn0addcom  43236  nn0mulcom  43240  fzsplit1nn0  43485  f1mo  49631