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  2602  moi2  2945  preq12bg  3804  ordsuc  4600  f1ocnv2d  6131  supisoti  7085  caucvgsrlemoffres  7886  prodge0  8900  un0addcl  9301  un0mulcl  9302  peano2uz2  9452  elfz2nn0  10206  fzind2  10334  expaddzap  10694  expmulzap  10696  cau3lem  11298  climuni  11477  climrecvg1n  11532  fisumcom2  11622  fprodcom2fi  11810  dvdsval2  11974  algcvga  12246  lcmgcdlem  12272  divgcdcoprmex  12297  prmpwdvds  12551  isgrpinv  13258  dvdsrcl2  13733  islss4  14016  lspsnel6  14042  epttop  14434  cncnp  14574  cnconst  14578  bl2in  14747  metcnpi  14859  metcnpi2  14860  metcnpi3  14861  perfect  15345  lgsquad2  15432