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  2649  moi2  3000  preq12bg  3879  ordsuc  4687  f1ocnv2d  6261  suppssrst  6463  suppssrgst  6464  supisoti  7303  caucvgsrlemoffres  8120  prodge0  9133  un0addcl  9534  un0mulcl  9535  peano2uz2  9691  elfz2nn0  10453  fzind2  10592  expaddzap  10952  expmulzap  10954  swrdswrd  11405  cau3lem  11807  climuni  11986  climrecvg1n  12041  fisumcom2  12132  fprodcom2fi  12320  dvdsval2  12484  algcvga  12756  lcmgcdlem  12782  divgcdcoprmex  12807  prmpwdvds  13061  isgrpinv  13788  dvdsrcl2  14266  islss4  14579  lspsnel6  14605  epttop  15004  cncnp  15144  cnconst  15148  bl2in  15317  metcnpi  15429  metcnpi2  15430  metcnpi3  15431  perfect  15918  lgsquad2  16005  egrsubgr  16307  clwwlkccat  16445  gfsumval  16911