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  2611  moi2  2954  preq12bg  3814  ordsuc  4611  f1ocnv2d  6150  supisoti  7112  caucvgsrlemoffres  7913  prodge0  8927  un0addcl  9328  un0mulcl  9329  peano2uz2  9480  elfz2nn0  10234  fzind2  10368  expaddzap  10728  expmulzap  10730  cau3lem  11425  climuni  11604  climrecvg1n  11659  fisumcom2  11749  fprodcom2fi  11937  dvdsval2  12101  algcvga  12373  lcmgcdlem  12399  divgcdcoprmex  12424  prmpwdvds  12678  isgrpinv  13386  dvdsrcl2  13861  islss4  14144  lspsnel6  14170  epttop  14562  cncnp  14702  cnconst  14706  bl2in  14875  metcnpi  14987  metcnpi2  14988  metcnpi3  14989  perfect  15473  lgsquad2  15560