Theorem impr 372

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  reximddv2  2478  moi2  2797  preq12bg  3623  ordsuc  4392  f1ocnv2d  5862  supisoti  6759  caucvgsrlemoffres  7406  prodge0  8376  un0addcl  8767  un0mulcl  8768  peano2uz2  8914  elfz2nn0  9587  fzind2  9711  expaddzap  10060  expmulzap  10062  cau3lem  10608  climuni  10742  climrecvg1n  10798  fisumcom2  10893  dvdsval2  11138  algcvga  11372  lcmgcdlem  11398  divgcdcoprmex  11423  epttop  11851