Theorem imp32 418

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

Hypothesis

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

Assertion

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

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp31.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 410	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  imp42  426  impr  454  anasss  466  an13s  651  3expb  1120  reuss2  4278  reupick  4281  po2nr  5546  tz7.7  6343  ordtr2  6362  fvmptt  6961  fliftfund  7259  isomin  7283  f1ocnv2d  7611  onint  7735  resf1extb  7876  soseq  8101  tz7.48lem  8372  oalimcl  8487  oaass  8488  omass  8507  omabs  8579  finsschain  9259  frmin  9661  infxpenlem  9923  axcc3  10348  zorn2lem7  10412  addclpi  10803  addnidpi  10812  genpnnp  10916  genpnmax  10918  mulclprlem  10930  dedekindle  11297  prodgt0  11988  ltsubrp  12943  ltaddrp  12944  pfxccat3  14657  sumeven  16314  sumodd  16315  lcmfunsnlem2lem1  16565  divgcdcoprm0  16592  infpnlem1  16838  prmgaplem4  16982  iscatd  17596  imasmnd2  18699  imasgrp2  18985  cyccom  19132  imasrng  20112  imasring  20266  funcrngcsetcALT  20574  mplcoe5lem  21994  dmatmul  22441  scmatmulcl  22462  scmatsgrp1  22466  smatvscl  22468  cpmatacl  22660  cpmatmcllem  22662  0ntr  23015  clsndisj  23019  innei  23069  islpi  23093  tgcnp  23197  haust1  23296  alexsublem  23988  alexsubb  23990  isxmetd  24270  bddiblnc  25799  2lgslem1a1  27356  nodense  27660  precsexlem11  28213  bdaypw2n0bndlem  28459  axcontlem4  29040  ewlkle  29679  clwwlkf  30122  clwwlknonwwlknonb  30181  uhgr3cyclexlem  30256  numclwwlk1lem2foa  30429  grpoidinvlem3  30581  elspansn5  31649  5oalem6  31734  mdi  32370  dmdi  32377  dmdsl3  32390  atom1d  32428  cvexchlem  32443  atcvatlem  32460  chirredlem3  32467  mdsymlem5  32482  f1o3d  32704  bnj570  35061  dfon2lem6  35980  broutsideof2  36316  outsideoftr  36323  outsideofeq  36324  elicc3  36511  nn0prpwlem  36516  nndivsub  36651  fvineqsneu  37616  fvineqsneq  37617  ftc1anc  37902  cntotbnd  37997  heiborlem6  38017  pridlc3  38274  erimeq2  38937  leat2  39554  cvrexchlem  39679  cvratlem  39681  3dim2  39728  ps-2  39738  lncvrelatN  40041  osumcllem11N  40226  relpmin  45193  2reuimp0  47360  iccpartgt  47673  odz2prm2pw  47809  bgoldbachlt  48059  tgblthelfgott  48061  tgoldbach  48063  grimco  48135  isubgr3stgrlem6  48217  isubgr3stgrlem8  48219  uspgrlimlem2  48235  clnbgr3stgrgrlic  48266  gpgedgvtx0  48307  gpgedgvtx1  48308