Theorem jaoian 959

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 858	. 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒))
6	5	imp 406	1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)

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

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 849

This theorem is referenced by:  ccase  1038  preq12nebg  4863  opthprneg  4865  elpreqpr  4867  tpres  7221  xaddnemnf  13278  xaddnepnf  13279  faclbnd  14329  faclbnd3  14331  faclbnd4lem1  14332  znf1o  21570  degltlem1  26111  ipasslem3  30852  padct  32731  fz1nntr  32806  xrge0iifhom  33936  bj-ideqg1ALT  37166  nn0addcom  42480  nn0mulcom  42484  fzsplit1nn0  42765  f1mo  48762