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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reximddv2  2655  moi2  3007  preq12bg  3898  ordsuc  4712  f1ocnv2d  6297  f1o3d  6301  suppssrst  6505  suppssrgst  6506  supisoti  7356  caucvgsrlemoffres  8173  prodge0  9192  un0addcl  9607  un0mulcl  9608  peano2uz2  9763  elfz2nn0  10535  fzind2  10674  expaddzap  11040  expmulzap  11042  swrdswrd  11498  cau3lem  11902  fiidxsupcl  12017  climuni  12083  climrecvg1n  12138  fisumcom2  12229  fprodcom2fi  12417  dvdsval2  12581  algcvga  12853  lcmgcdlem  12879  divgcdcoprmex  12904  prmpwdvds  13162  isgrpinv  13917  gsumvalfi  14241  dvdsrcl2  14514  islss4  14827  ellspsn6  14853  gsumbagdiagfi  15185  psrass1filem  15186  epttop  15333  cncnp  15473  cnconst  15477  bl2in  15646  metcnpi  15758  metcnpi2  15759  metcnpi3  15760  perfect  16318  bposlem1  16328  lgsquad2  16424  egrsubgr  16726  clwwlkccat  16864