Theorem impr 379

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 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 257	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  reximddv2  2582  moi2  2919  preq12bg  3774  ordsuc  4563  f1ocnv2d  6075  supisoti  7009  caucvgsrlemoffres  7799  prodge0  8811  un0addcl  9209  un0mulcl  9210  peano2uz2  9360  elfz2nn0  10112  fzind2  10239  expaddzap  10564  expmulzap  10566  cau3lem  11123  climuni  11301  climrecvg1n  11356  fisumcom2  11446  fprodcom2fi  11634  dvdsval2  11797  algcvga  12051  lcmgcdlem  12077  divgcdcoprmex  12102  prmpwdvds  12353  isgrpinv  12926  dvdsrcl2  13268  epttop  13593  cncnp  13733  cnconst  13737  bl2in  13906  metcnpi  14018  metcnpi2  14019  metcnpi3  14020