Theorem jaoian 969

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  ccase  1048  preq12nebg  4818  opthprneg  4820  elpreqpr  4822  tpres  7180  xaddnemnf  13233  xaddnepnf  13234  faclbnd  14297  faclbnd3  14299  faclbnd4lem1  14300  znf1o  21591  degltlem1  26120  ipasslem3  30993  padct  32881  fz1nntr  32965  xrge0iifhom  34195  bj-ideqg1ALT  37618  nn0addcom  43045  nn0mulcom  43049  fzsplit1nn0  43296  f1mo  49435