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  2985  preq12bg  3854  ordsuc  4659  f1ocnv2d  6222  supisoti  7200  caucvgsrlemoffres  8010  prodge0  9024  un0addcl  9425  un0mulcl  9426  peano2uz2  9577  elfz2nn0  10337  fzind2  10475  expaddzap  10835  expmulzap  10837  swrdswrd  11276  cau3lem  11665  climuni  11844  climrecvg1n  11899  fisumcom2  11989  fprodcom2fi  12177  dvdsval2  12341  algcvga  12613  lcmgcdlem  12639  divgcdcoprmex  12664  prmpwdvds  12918  isgrpinv  13627  dvdsrcl2  14103  islss4  14386  lspsnel6  14412  epttop  14804  cncnp  14944  cnconst  14948  bl2in  15117  metcnpi  15229  metcnpi2  15230  metcnpi3  15231  perfect  15715  lgsquad2  15802  clwwlkccat  16196