Theorem impr 376

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 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  reximddv2  2535  moi2  2860  preq12bg  3695  ordsuc  4473  f1ocnv2d  5967  supisoti  6890  caucvgsrlemoffres  7601  prodge0  8605  un0addcl  9003  un0mulcl  9004  peano2uz2  9151  elfz2nn0  9885  fzind2  10009  expaddzap  10330  expmulzap  10332  cau3lem  10879  climuni  11055  climrecvg1n  11110  fisumcom2  11200  dvdsval2  11485  algcvga  11721  lcmgcdlem  11747  divgcdcoprmex  11772  epttop  12248  cncnp  12388  cnconst  12392  bl2in  12561  metcnpi  12673  metcnpi2  12674  metcnpi3  12675