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  6210  supisoti  7177  caucvgsrlemoffres  7987  prodge0  9001  un0addcl  9402  un0mulcl  9403  peano2uz2  9554  elfz2nn0  10308  fzind2  10445  expaddzap  10805  expmulzap  10807  swrdswrd  11237  cau3lem  11625  climuni  11804  climrecvg1n  11859  fisumcom2  11949  fprodcom2fi  12137  dvdsval2  12301  algcvga  12573  lcmgcdlem  12599  divgcdcoprmex  12624  prmpwdvds  12878  isgrpinv  13587  dvdsrcl2  14063  islss4  14346  lspsnel6  14372  epttop  14764  cncnp  14904  cnconst  14908  bl2in  15077  metcnpi  15189  metcnpi2  15190  metcnpi3  15191  perfect  15675  lgsquad2  15762