Theorem impr 371

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  reximddv2  2465  moi2  2773  preq12bg  3565  ordsuc  4306  f1ocnv2d  5724  supisoti  6423  caucvgsrlemoffres  6976  prodge0  7932  un0addcl  8321  un0mulcl  8322  peano2uz2  8454  elfz2nn0  9128  fzind2  9248  expaddzap  9520  expmulzap  9522  cau3lem  10000  climuni  10132  climrecvg1n  10185  dvdsval2  10198  ialgcvga  10433  lcmgcdlem  10459  divgcdcoprmex  10484