Theorem impr 377

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  2540  moi2  2869  preq12bg  3708  ordsuc  4486  f1ocnv2d  5982  supisoti  6905  caucvgsrlemoffres  7632  prodge0  8636  un0addcl  9034  un0mulcl  9035  peano2uz2  9182  elfz2nn0  9923  fzind2  10047  expaddzap  10368  expmulzap  10370  cau3lem  10918  climuni  11094  climrecvg1n  11149  fisumcom2  11239  dvdsval2  11532  algcvga  11768  lcmgcdlem  11794  divgcdcoprmex  11819  epttop  12298  cncnp  12438  cnconst  12442  bl2in  12611  metcnpi  12723  metcnpi2  12724  metcnpi3  12725