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  2635  moi2  2984  preq12bg  3851  ordsuc  4655  f1ocnv2d  6216  supisoti  7188  caucvgsrlemoffres  7998  prodge0  9012  un0addcl  9413  un0mulcl  9414  peano2uz2  9565  elfz2nn0  10320  fzind2  10457  expaddzap  10817  expmulzap  10819  swrdswrd  11253  cau3lem  11641  climuni  11820  climrecvg1n  11875  fisumcom2  11965  fprodcom2fi  12153  dvdsval2  12317  algcvga  12589  lcmgcdlem  12615  divgcdcoprmex  12640  prmpwdvds  12894  isgrpinv  13603  dvdsrcl2  14079  islss4  14362  lspsnel6  14388  epttop  14780  cncnp  14920  cnconst  14924  bl2in  15093  metcnpi  15205  metcnpi2  15206  metcnpi3  15207  perfect  15691  lgsquad2  15778  clwwlkccat  16144