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  7200  xaddnemnf  13288  xaddnepnf  13289  faclbnd  14354  faclbnd3  14356  faclbnd4lem1  14357  znf1o  21764  degltlem1  26297  ipasslem3  31314  padct  33189  fz1nntr  33273  xrge0iifhom  34447  bj-ideqg1ALT  37917  nn0addcom  43350  nn0mulcom  43354  fzsplit1nn0  43599  f1mo  49781