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  2602  moi2  2945  preq12bg  3803  ordsuc  4599  f1ocnv2d  6127  supisoti  7076  caucvgsrlemoffres  7867  prodge0  8881  un0addcl  9282  un0mulcl  9283  peano2uz2  9433  elfz2nn0  10187  fzind2  10315  expaddzap  10675  expmulzap  10677  cau3lem  11279  climuni  11458  climrecvg1n  11513  fisumcom2  11603  fprodcom2fi  11791  dvdsval2  11955  algcvga  12219  lcmgcdlem  12245  divgcdcoprmex  12270  prmpwdvds  12524  isgrpinv  13186  dvdsrcl2  13655  islss4  13938  lspsnel6  13964  epttop  14326  cncnp  14466  cnconst  14470  bl2in  14639  metcnpi  14751  metcnpi2  14752  metcnpi3  14753  perfect  15237  lgsquad2  15324