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  2613  moi2  2961  preq12bg  3827  ordsuc  4629  f1ocnv2d  6173  supisoti  7138  caucvgsrlemoffres  7948  prodge0  8962  un0addcl  9363  un0mulcl  9364  peano2uz2  9515  elfz2nn0  10269  fzind2  10405  expaddzap  10765  expmulzap  10767  swrdswrd  11196  cau3lem  11540  climuni  11719  climrecvg1n  11774  fisumcom2  11864  fprodcom2fi  12052  dvdsval2  12216  algcvga  12488  lcmgcdlem  12514  divgcdcoprmex  12539  prmpwdvds  12793  isgrpinv  13501  dvdsrcl2  13976  islss4  14259  lspsnel6  14285  epttop  14677  cncnp  14817  cnconst  14821  bl2in  14990  metcnpi  15102  metcnpi2  15103  metcnpi3  15104  perfect  15588  lgsquad2  15675