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  4285  reupick  4288  po2nr  5553  tz7.7  6346  ordtr2  6365  fvmptt  6970  fliftfund  7270  isomin  7294  f1ocnv2d  7622  onint  7746  resf1extb  7890  soseq  8115  tz7.48lem  8386  oalimcl  8501  oaass  8502  omass  8521  omabs  8592  finsschain  9286  frmin  9678  infxpenlem  9942  axcc3  10367  zorn2lem7  10431  addclpi  10821  addnidpi  10830  genpnnp  10934  genpnmax  10936  mulclprlem  10948  dedekindle  11314  prodgt0  12005  ltsubrp  12965  ltaddrp  12966  pfxccat3  14675  sumeven  16333  sumodd  16334  lcmfunsnlem2lem1  16584  divgcdcoprm0  16611  infpnlem1  16857  prmgaplem4  17001  iscatd  17614  imasmnd2  18683  imasgrp2  18969  cyccom  19117  imasrng  20097  imasring  20250  funcrngcsetcALT  20561  mplcoe5lem  21979  dmatmul  22417  scmatmulcl  22438  scmatsgrp1  22442  smatvscl  22444  cpmatacl  22636  cpmatmcllem  22638  0ntr  22991  clsndisj  22995  innei  23045  islpi  23069  tgcnp  23173  haust1  23272  alexsublem  23964  alexsubb  23966  isxmetd  24247  bddiblnc  25776  2lgslem1a1  27333  nodense  27637  precsexlem11  28159  axcontlem4  28947  ewlkle  29586  clwwlkf  30026  clwwlknonwwlknonb  30085  uhgr3cyclexlem  30160  numclwwlk1lem2foa  30333  grpoidinvlem3  30485  elspansn5  31553  5oalem6  31638  mdi  32274  dmdi  32281  dmdsl3  32294  atom1d  32332  cvexchlem  32347  atcvatlem  32364  chirredlem3  32371  mdsymlem5  32386  f1o3d  32601  bnj570  34888  dfon2lem6  35769  broutsideof2  36103  outsideoftr  36110  outsideofeq  36111  elicc3  36298  nn0prpwlem  36303  nndivsub  36438  fvineqsneu  37392  fvineqsneq  37393  ftc1anc  37688  cntotbnd  37783  heiborlem6  37803  pridlc3  38060  erimeq2  38663  leat2  39280  cvrexchlem  39406  cvratlem  39408  3dim2  39455  ps-2  39465  lncvrelatN  39768  osumcllem11N  39953  relpmin  44935  2reuimp0  47108  iccpartgt  47421  odz2prm2pw  47557  bgoldbachlt  47807  tgblthelfgott  47809  tgoldbach  47811  grimco  47882  isubgr3stgrlem6  47963  isubgr3stgrlem8  47965  uspgrlimlem2  47981  clnbgr3stgrgrlic  48004  gpgedgvtx0  48045  gpgedgvtx1  48046