Theorem jaoian 958

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  ccase  1037  preq12nebg  4868  opthprneg  4870  elpreqpr  4872  tpres  7221  xaddnemnf  13275  xaddnepnf  13276  faclbnd  14326  faclbnd3  14328  faclbnd4lem1  14329  znf1o  21588  degltlem1  26126  ipasslem3  30862  padct  32737  fz1nntr  32812  xrge0iifhom  33898  bj-ideqg1ALT  37148  nn0addcom  42457  nn0mulcom  42461  fzsplit1nn0  42742  f1mo  48683