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  2647  moi2  2997  preq12bg  3870  ordsuc  4676  f1ocnv2d  6250  suppssrst  6452  suppssrgst  6453  supisoti  7292  caucvgsrlemoffres  8103  prodge0  9116  un0addcl  9517  un0mulcl  9518  peano2uz2  9671  elfz2nn0  10432  fzind2  10571  expaddzap  10931  expmulzap  10933  swrdswrd  11375  cau3lem  11777  climuni  11956  climrecvg1n  12011  fisumcom2  12102  fprodcom2fi  12290  dvdsval2  12454  algcvga  12726  lcmgcdlem  12752  divgcdcoprmex  12777  prmpwdvds  13031  isgrpinv  13741  dvdsrcl2  14218  islss4  14502  lspsnel6  14528  epttop  14925  cncnp  15065  cnconst  15069  bl2in  15238  metcnpi  15350  metcnpi2  15351  metcnpi3  15352  perfect  15839  lgsquad2  15926  egrsubgr  16228  clwwlkccat  16366  gfsumval  16831