Theorem jaoian 964

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  ccase  1043  preq12nebg  4794  opthprneg  4796  elpreqpr  4798  tpres  7145  xaddnemnf  13179  xaddnepnf  13180  faclbnd  14243  faclbnd3  14245  faclbnd4lem1  14246  znf1o  21526  degltlem1  26055  ipasslem3  30922  padct  32810  fz1nntr  32894  xrge0iifhom  34121  bj-ideqg1ALT  37525  nn0addcom  42952  nn0mulcom  42956  fzsplit1nn0  43203  f1mo  49343