Theorem imp32 257

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp32	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 254	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 124	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

This theorem is referenced by:  imp42  354  impr  379  anasss  399  an13s  569  3expb  1231  reuss2  3503  reupick  3507  po2nr  4432  fvmptt  5771  fliftfund  5972  f1ocnv2d  6261  addclpi  7644  addnidpig  7653  mulnqprl  7885  mulnqpru  7886  ltsubrp  10026  ltaddrp  10027  pfxccat3  11430  divgcdcoprm0  12802  infpnlem1  13061  imasmnd2  13682  imasgrp2  13844  imasrng  14117  imasring  14225  innei  15045  tgcnp  15091  isxmetd  15229  2lgslem1a1  15976