Theorem impr 376

Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
impr.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem impr

Step	Hyp	Ref	Expression
1		impr.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  reximddv2  2537  moi2  2865  preq12bg  3700  ordsuc  4478  f1ocnv2d  5974  supisoti  6897  caucvgsrlemoffres  7608  prodge0  8612  un0addcl  9010  un0mulcl  9011  peano2uz2  9158  elfz2nn0  9892  fzind2  10016  expaddzap  10337  expmulzap  10339  cau3lem  10886  climuni  11062  climrecvg1n  11117  fisumcom2  11207  dvdsval2  11496  algcvga  11732  lcmgcdlem  11758  divgcdcoprmex  11783  epttop  12259  cncnp  12399  cnconst  12403  bl2in  12572  metcnpi  12684  metcnpi2  12685  metcnpi3  12686