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  6230  supisoti  7212  caucvgsrlemoffres  8023  prodge0  9037  un0addcl  9438  un0mulcl  9439  peano2uz2  9590  elfz2nn0  10350  fzind2  10489  expaddzap  10849  expmulzap  10851  swrdswrd  11293  cau3lem  11695  climuni  11874  climrecvg1n  11929  fisumcom2  12020  fprodcom2fi  12208  dvdsval2  12372  algcvga  12644  lcmgcdlem  12670  divgcdcoprmex  12695  prmpwdvds  12949  isgrpinv  13658  dvdsrcl2  14135  islss4  14418  lspsnel6  14444  epttop  14841  cncnp  14981  cnconst  14985  bl2in  15154  metcnpi  15266  metcnpi2  15267  metcnpi3  15268  perfect  15752  lgsquad2  15839  egrsubgr  16141  clwwlkccat  16279  gfsumval  16740