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  4817  opthprneg  4819  elpreqpr  4821  tpres  7211  xaddnemnf  13373  xaddnepnf  13374  faclbnd  14441  faclbnd3  14443  faclbnd4lem1  14444  znf1o  21866  degltlem1  26399  ipasslem3  31444  padct  33361  fz1nntr  33444  xrge0iifhom  34619  bj-ideqg1ALT  38195  nn0addcom  43635  nn0mulcom  43639  fzsplit1nn0  43874  f1mo  50072