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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  ccase  1053  preq12nebg  4830  opthprneg  4832  elpreqpr  4834  tpres  7203  xaddnemnf  13274  xaddnepnf  13275  faclbnd  14340  faclbnd3  14342  faclbnd4lem1  14343  znf1o  21731  degltlem1  26260  ipasslem3  31232  padct  33109  fz1nntr  33193  xrge0iifhom  34367  bj-ideqg1ALT  37842  nn0addcom  43269  nn0mulcom  43273  fzsplit1nn0  43518  f1mo  49664