Theorem jaoian 957

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

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

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 847

This theorem is referenced by:  ccase  1038  preq12nebg  4887  opthprneg  4889  elpreqpr  4891  tpres  7238  xaddnemnf  13298  xaddnepnf  13299  faclbnd  14339  faclbnd3  14341  faclbnd4lem1  14342  znf1o  21593  degltlem1  26131  ipasslem3  30865  padct  32733  fz1nntr  32809  xrge0iifhom  33883  bj-ideqg1ALT  37131  nn0addcom  42426  nn0mulcom  42430  fzsplit1nn0  42710  f1mo  48566