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  4301  reupick  4304  po2nr  5575  tz7.7  6378  ordtr2  6397  fvmptt  7005  fliftfund  7305  isomin  7329  f1ocnv2d  7658  onint  7782  resf1extb  7928  soseq  8156  tz7.48lem  8453  oalimcl  8570  oaass  8571  omass  8590  omabs  8661  finsschain  9369  frmin  9761  infxpenlem  10025  axcc3  10450  zorn2lem7  10514  addclpi  10904  addnidpi  10913  genpnnp  11017  genpnmax  11019  mulclprlem  11031  dedekindle  11397  prodgt0  12086  ltsubrp  13043  ltaddrp  13044  pfxccat3  14750  sumeven  16404  sumodd  16405  lcmfunsnlem2lem1  16655  divgcdcoprm0  16682  infpnlem1  16928  prmgaplem4  17072  iscatd  17683  imasmnd2  18750  imasgrp2  19036  cyccom  19184  imasrng  20135  imasring  20288  funcrngcsetcALT  20599  mplcoe5lem  21995  dmatmul  22433  scmatmulcl  22454  scmatsgrp1  22458  smatvscl  22460  cpmatacl  22652  cpmatmcllem  22654  0ntr  23007  clsndisj  23011  innei  23061  islpi  23085  tgcnp  23189  haust1  23288  alexsublem  23980  alexsubb  23982  isxmetd  24263  bddiblnc  25793  2lgslem1a1  27350  nodense  27654  precsexlem11  28158  axcontlem4  28892  ewlkle  29531  clwwlkf  29974  clwwlknonwwlknonb  30033  uhgr3cyclexlem  30108  numclwwlk1lem2foa  30281  grpoidinvlem3  30433  elspansn5  31501  5oalem6  31586  mdi  32222  dmdi  32229  dmdsl3  32242  atom1d  32280  cvexchlem  32295  atcvatlem  32312  chirredlem3  32319  mdsymlem5  32334  f1o3d  32551  bnj570  34882  dfon2lem6  35752  broutsideof2  36086  outsideoftr  36093  outsideofeq  36094  elicc3  36281  nn0prpwlem  36286  nndivsub  36421  fvineqsneu  37375  fvineqsneq  37376  ftc1anc  37671  cntotbnd  37766  heiborlem6  37786  pridlc3  38043  erimeq2  38642  leat2  39258  cvrexchlem  39384  cvratlem  39386  3dim2  39433  ps-2  39443  lncvrelatN  39746  osumcllem11N  39931  relpmin  44925  2reuimp0  47091  iccpartgt  47389  odz2prm2pw  47525  bgoldbachlt  47775  tgblthelfgott  47777  tgoldbach  47779  grimco  47850  isubgr3stgrlem6  47931  isubgr3stgrlem8  47933  uspgrlimlem2  47949  clnbgr3stgrgrlic  47972  gpgedgvtx0  48013  gpgedgvtx1  48014