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  17610  imasmnd2  18677  imasgrp2  18963  cyccom  19111  imasrng  20062  imasring  20215  funcrngcsetcALT  20526  mplcoe5lem  21922  dmatmul  22360  scmatmulcl  22381  scmatsgrp1  22385  smatvscl  22387  cpmatacl  22579  cpmatmcllem  22581  0ntr  22934  clsndisj  22938  innei  22988  islpi  23012  tgcnp  23116  haust1  23215  alexsublem  23907  alexsubb  23909  isxmetd  24190  bddiblnc  25719  2lgslem1a1  27276  nodense  27580  precsexlem11  28095  axcontlem4  28870  ewlkle  29509  clwwlkf  29949  clwwlknonwwlknonb  30008  uhgr3cyclexlem  30083  numclwwlk1lem2foa  30256  grpoidinvlem3  30408  elspansn5  31476  5oalem6  31561  mdi  32197  dmdi  32204  dmdsl3  32217  atom1d  32255  cvexchlem  32270  atcvatlem  32287  chirredlem3  32294  mdsymlem5  32309  f1o3d  32524  bnj570  34868  dfon2lem6  35749  broutsideof2  36083  outsideoftr  36090  outsideofeq  36091  elicc3  36278  nn0prpwlem  36283  nndivsub  36418  fvineqsneu  37372  fvineqsneq  37373  ftc1anc  37668  cntotbnd  37763  heiborlem6  37783  pridlc3  38040  erimeq2  38643  leat2  39260  cvrexchlem  39386  cvratlem  39388  3dim2  39435  ps-2  39445  lncvrelatN  39748  osumcllem11N  39933  relpmin  44915  2reuimp0  47088  iccpartgt  47401  odz2prm2pw  47537  bgoldbachlt  47787  tgblthelfgott  47789  tgoldbach  47791  grimco  47862  isubgr3stgrlem6  47943  isubgr3stgrlem8  47945  uspgrlimlem2  47961  clnbgr3stgrgrlic  47984  gpgedgvtx0  48025  gpgedgvtx1  48026