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  1228  reuss2  3485  reupick  3489  po2nr  4404  fvmptt  5734  fliftfund  5933  f1ocnv2d  6222  addclpi  7537  addnidpig  7546  mulnqprl  7778  mulnqpru  7779  ltsubrp  9915  ltaddrp  9916  pfxccat3  11305  divgcdcoprm0  12663  infpnlem1  12922  imasmnd2  13525  imasgrp2  13687  imasrng  13959  imasring  14067  innei  14877  tgcnp  14923  isxmetd  15061  2lgslem1a1  15805