Theorem impr 377

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  2559  moi2  2889  preq12bg  3732  ordsuc  4516  f1ocnv2d  6014  supisoti  6942  caucvgsrlemoffres  7699  prodge0  8704  un0addcl  9102  un0mulcl  9103  peano2uz2  9250  elfz2nn0  9992  fzind2  10116  expaddzap  10441  expmulzap  10443  cau3lem  10991  climuni  11167  climrecvg1n  11222  fisumcom2  11312  fprodcom2fi  11500  dvdsval2  11663  algcvga  11899  lcmgcdlem  11925  divgcdcoprmex  11950  epttop  12429  cncnp  12569  cnconst  12573  bl2in  12742  metcnpi  12854  metcnpi2  12855  metcnpi3  12856