Theorem jaoian 953

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

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843

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 399  df-or 844

This theorem is referenced by:  ccase  1032  preq12nebg  4774  opthprneg  4776  elpreqpr  4778  tpres  6944  xaddnemnf  12611  xaddnepnf  12612  faclbnd  13635  faclbnd3  13637  faclbnd4lem1  13638  znf1o  20676  degltlem1  24647  ipasslem3  28589  padct  30436  fz1nntr  30508  xrge0iifhom  31182  bj-ideqg1ALT  34468  fzsplit1nn0  39438