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  4710  f1ocnv2d  6294  f1o3d  6298  suppssrst  6501  suppssrgst  6502  supisoti  7351  caucvgsrlemoffres  8168  prodge0  9187  un0addcl  9601  un0mulcl  9602  peano2uz2  9758  elfz2nn0  10530  fzind2  10669  expaddzap  11035  expmulzap  11037  swrdswrd  11493  cau3lem  11897  fiidxsupcl  12012  climuni  12078  climrecvg1n  12133  fisumcom2  12224  fprodcom2fi  12412  dvdsval2  12576  algcvga  12848  lcmgcdlem  12874  divgcdcoprmex  12899  prmpwdvds  13157  isgrpinv  13912  gsumvalfi  14236  dvdsrcl2  14490  islss4  14803  ellspsn6  14829  epttop  15282  cncnp  15422  cnconst  15426  bl2in  15595  metcnpi  15707  metcnpi2  15708  metcnpi3  15709  perfect  16267  bposlem1  16277  lgsquad2  16373  egrsubgr  16675  clwwlkccat  16813