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  4823  opthprneg  4825  elpreqpr  4827  tpres  7238  xaddnemnf  13406  xaddnepnf  13407  faclbnd  14475  faclbnd3  14477  faclbnd4lem1  14478  znf1o  21912  degltlem1  26445  ipasslem3  31492  padct  33407  fz1nntr  33490  xrge0iifhom  34680  bj-ideqg1ALT  38354  nn0addcom  43792  nn0mulcom  43796  fzsplit1nn0  44031  f1mo  50295