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  567  3expb  1207  reuss2  3457  reupick  3461  po2nr  4364  fvmptt  5684  fliftfund  5879  f1ocnv2d  6163  addclpi  7460  addnidpig  7469  mulnqprl  7701  mulnqpru  7702  ltsubrp  9832  ltaddrp  9833  divgcdcoprm0  12498  infpnlem1  12757  imasmnd2  13359  imasgrp2  13521  imasrng  13793  imasring  13901  innei  14710  tgcnp  14756  isxmetd  14894  2lgslem1a1  15638