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  1121  reuss2  4326  reupick  4329  po2nr  5606  tz7.7  6410  ordtr2  6428  fvmptt  7036  fliftfund  7333  isomin  7357  f1ocnv2d  7686  onint  7810  resf1extb  7956  soseq  8184  tz7.48lem  8481  oalimcl  8598  oaass  8599  omass  8618  omabs  8689  finsschain  9399  frmin  9789  infxpenlem  10053  axcc3  10478  zorn2lem7  10542  addclpi  10932  addnidpi  10941  genpnnp  11045  genpnmax  11047  mulclprlem  11059  dedekindle  11425  prodgt0  12114  ltsubrp  13071  ltaddrp  13072  pfxccat3  14772  sumeven  16424  sumodd  16425  lcmfunsnlem2lem1  16675  divgcdcoprm0  16702  infpnlem1  16948  prmgaplem4  17092  iscatd  17716  imasmnd2  18787  imasgrp2  19073  cyccom  19221  imasrng  20174  imasring  20327  funcrngcsetcALT  20641  mplcoe5lem  22057  dmatmul  22503  scmatmulcl  22524  scmatsgrp1  22528  smatvscl  22530  cpmatacl  22722  cpmatmcllem  22724  0ntr  23079  clsndisj  23083  innei  23133  islpi  23157  tgcnp  23261  haust1  23360  alexsublem  24052  alexsubb  24054  isxmetd  24336  bddiblnc  25877  2lgslem1a1  27433  nodense  27737  precsexlem11  28241  axcontlem4  28982  ewlkle  29623  clwwlkf  30066  clwwlknonwwlknonb  30125  uhgr3cyclexlem  30200  numclwwlk1lem2foa  30373  grpoidinvlem3  30525  elspansn5  31593  5oalem6  31678  mdi  32314  dmdi  32321  dmdsl3  32334  atom1d  32372  cvexchlem  32387  atcvatlem  32404  chirredlem3  32411  mdsymlem5  32426  f1o3d  32637  bnj570  34919  dfon2lem6  35789  broutsideof2  36123  outsideoftr  36130  outsideofeq  36131  elicc3  36318  nn0prpwlem  36323  nndivsub  36458  fvineqsneu  37412  fvineqsneq  37413  ftc1anc  37708  cntotbnd  37803  heiborlem6  37823  pridlc3  38080  erimeq2  38679  leat2  39295  cvrexchlem  39421  cvratlem  39423  3dim2  39470  ps-2  39480  lncvrelatN  39783  osumcllem11N  39968  relpmin  44973  2reuimp0  47126  iccpartgt  47414  odz2prm2pw  47550  bgoldbachlt  47800  tgblthelfgott  47802  tgoldbach  47804  grimco  47880  isubgr3stgrlem6  47938  isubgr3stgrlem8  47940  uspgrlimlem2  47956  clnbgr3stgrgrlic  47979  gpgedgvtx0  48019  gpgedgvtx1  48020