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  2637  moi2  2987  preq12bg  3856  ordsuc  4661  f1ocnv2d  6226  supisoti  7208  caucvgsrlemoffres  8019  prodge0  9033  un0addcl  9434  un0mulcl  9435  peano2uz2  9586  elfz2nn0  10346  fzind2  10484  expaddzap  10844  expmulzap  10846  swrdswrd  11285  cau3lem  11674  climuni  11853  climrecvg1n  11908  fisumcom2  11998  fprodcom2fi  12186  dvdsval2  12350  algcvga  12622  lcmgcdlem  12648  divgcdcoprmex  12673  prmpwdvds  12927  isgrpinv  13636  dvdsrcl2  14112  islss4  14395  lspsnel6  14421  epttop  14813  cncnp  14953  cnconst  14957  bl2in  15126  metcnpi  15238  metcnpi2  15239  metcnpi3  15240  perfect  15724  lgsquad2  15811  egrsubgr  16113  clwwlkccat  16251  gfsumval  16680