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  1119  reuss2  4331  reupick  4334  po2nr  5610  tz7.7  6411  ordtr2  6429  fvmptt  7035  fliftfund  7332  isomin  7356  f1ocnv2d  7685  onint  7809  soseq  8182  tz7.48lem  8479  oalimcl  8596  oaass  8597  omass  8616  omabs  8687  finsschain  9396  frmin  9786  infxpenlem  10050  axcc3  10475  zorn2lem7  10539  addclpi  10929  addnidpi  10938  genpnnp  11042  genpnmax  11044  mulclprlem  11056  dedekindle  11422  prodgt0  12111  ltsubrp  13068  ltaddrp  13069  pfxccat3  14768  sumeven  16420  sumodd  16421  lcmfunsnlem2lem1  16671  divgcdcoprm0  16698  infpnlem1  16943  prmgaplem4  17087  iscatd  17717  imasmnd2  18799  imasgrp2  19085  cyccom  19233  imasrng  20194  imasring  20343  funcrngcsetcALT  20657  mplcoe5lem  22074  dmatmul  22518  scmatmulcl  22539  scmatsgrp1  22543  smatvscl  22545  cpmatacl  22737  cpmatmcllem  22739  0ntr  23094  clsndisj  23098  innei  23148  islpi  23172  tgcnp  23276  haust1  23375  alexsublem  24067  alexsubb  24069  isxmetd  24351  bddiblnc  25891  2lgslem1a1  27447  nodense  27751  precsexlem11  28255  axcontlem4  28996  ewlkle  29637  clwwlkf  30075  clwwlknonwwlknonb  30134  uhgr3cyclexlem  30209  numclwwlk1lem2foa  30382  grpoidinvlem3  30534  elspansn5  31602  5oalem6  31687  mdi  32323  dmdi  32330  dmdsl3  32343  atom1d  32381  cvexchlem  32396  atcvatlem  32413  chirredlem3  32420  mdsymlem5  32435  f1o3d  32643  bnj570  34897  dfon2lem6  35769  broutsideof2  36103  outsideoftr  36110  outsideofeq  36111  elicc3  36299  nn0prpwlem  36304  nndivsub  36439  fvineqsneu  37393  fvineqsneq  37394  ftc1anc  37687  cntotbnd  37782  heiborlem6  37802  pridlc3  38059  erimeq2  38659  leat2  39275  cvrexchlem  39401  cvratlem  39403  3dim2  39450  ps-2  39460  lncvrelatN  39763  osumcllem11N  39948  2reuimp0  47063  iccpartgt  47351  odz2prm2pw  47487  bgoldbachlt  47737  tgblthelfgott  47739  tgoldbach  47741  grimco  47817  isubgr3stgrlem6  47873  isubgr3stgrlem8  47875  uspgrlimlem2  47891  clnbgr3stgrgrlic  47914  gpgedgvtx0  47953  gpgedgvtx1  47954