Theorem imp32 419

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 411	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 407	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp42  427  impr  455  anasss  467  an13s  657  3expb  1126  reuss2  4254  reupick  4257  po2nr  5540  tz7.7  6336  ordtr2  6355  fvmptt  6956  fliftfund  7257  isomin  7281  f1ocnv2d  7609  onint  7733  resf1extb  7874  soseq  8099  tz7.48lem  8370  oalimcl  8485  oaass  8486  omass  8505  omabs  8577  finsschain  9259  frmin  9664  infxpenlem  9926  axcc3  10351  zorn2lem7  10415  addclpi  10806  addnidpi  10815  genpnnp  10919  genpnmax  10921  mulclprlem  10933  dedekindle  11301  prodgt0  11993  ltsubrp  12971  ltaddrp  12972  pfxccat3  14687  sumeven  16347  sumodd  16348  lcmfunsnlem2lem1  16598  divgcdcoprm0  16625  infpnlem1  16872  prmgaplem4  17016  iscatd  17630  imasmnd2  18733  imasgrp2  19022  cyccom  19169  imasrng  20149  imasring  20301  funcrngcsetcALT  20613  mplcoe5lem  22015  dmatmul  22480  scmatmulcl  22501  scmatsgrp1  22505  smatvscl  22507  cpmatacl  22699  cpmatmcllem  22701  0ntr  23054  clsndisj  23058  innei  23108  islpi  23132  tgcnp  23236  haust1  23335  alexsublem  24027  alexsubb  24029  isxmetd  24309  bddiblnc  25827  2lgslem1a1  27370  nodense  27674  precsexlem11  28227  bdaypw2n0bndlem  28473  axcontlem4  29054  ewlkle  29692  clwwlkf  30135  clwwlknonwwlknonb  30194  uhgr3cyclexlem  30269  numclwwlk1lem2foa  30442  grpoidinvlem3  30595  elspansn5  31663  5oalem6  31748  mdi  32384  dmdi  32391  dmdsl3  32404  atom1d  32442  cvexchlem  32457  atcvatlem  32474  chirredlem3  32481  mdsymlem5  32496  f1o3d  32718  bnj570  35087  dfon2lem6  36014  broutsideof2  36350  outsideoftr  36357  outsideofeq  36358  elicc3  36545  nn0prpwlem  36550  nndivsub  36685  fvineqsneu  37773  fvineqsneq  37774  ftc1anc  38068  cntotbnd  38163  heiborlem6  38183  pridlc3  38440  erimeq2  39130  leat2  39786  cvrexchlem  39911  cvratlem  39913  3dim2  39960  ps-2  39970  lncvrelatN  40273  osumcllem11N  40458  relpmin  45396  2reuimp0  47577  iccpartgt  47902  odz2prm2pw  48041  bgoldbachlt  48304  tgblthelfgott  48306  tgoldbach  48308  grimco  48380  isubgr3stgrlem6  48462  isubgr3stgrlem8  48464  uspgrlimlem2  48480  clnbgr3stgrgrlic  48511  gpgedgvtx0  48552  gpgedgvtx1  48553