Theorem imp32 424

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 416	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 412	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp42  432  impr  460  anasss  472  an13s  664  3expb  1138  reuss2  4272  reupick  4275  po2nr  5573  tz7.7  6387  ordtr2  6407  fvmptt  7012  fliftfund  7319  isomin  7343  f1ocnv2d  7672  onint  7802  resf1extb  7944  soseq  8169  tz7.48lemOLD  8444  oalimcl  8561  oaass  8562  omass  8581  omabs  8653  finsschain  9341  frmin  9746  infxpenlem  10085  axcc3  10509  zorn2lem7  10573  addclpi  10970  addnidpi  10979  genpnnp  11083  genpnmax  11085  mulclprlem  11097  dedekindle  11467  prodgt0  12157  ltsubrp  13151  ltaddrp  13152  pfxccat3  14876  sumeven  16550  sumodd  16551  lcmfunsnlem2lem1  16806  divgcdcoprm0  16833  infpnlem1  17081  prmgaplem4  17225  iscatd  17840  mgmn0plusgf  18820  imasmnd2  18961  imasgrp2  19258  cyccom  19411  imasrng  20392  imasring  20553  funcrngcsetcALT  20886  cmprmidlmcl  21624  mplcoe5lem  22341  dmatmul  22805  scmatmulcl  22826  scmatsgrp1  22830  smatvscl  22832  cpmatacl  23027  cpmatmcllem  23029  0ntr  23382  clsndisj  23386  innei  23436  islpi  23460  tgcnp  23564  haust1  23663  alexsublem  24356  alexsubb  24358  isxmetd  24638  bddiblnc  26155  2lgslem1a1  27709  nodense  28042  precsexlem11  28596  bdaypw2n0bndlem  28842  axcontlem4  29538  ewlkle  30179  clwwlkf  30631  clwwlknonwwlknonb  30690  uhgr3cyclexlem  30775  numclwwlk1lem2foa  30948  grpoidinvlem3  31101  elspansn5  32169  5oalem6  32254  mdi  32890  dmdi  32897  dmdsl3  32910  atom1d  32948  cvexchlem  32963  atcvatlem  32980  chirredlem3  32987  mdsymlem5  33002  f1o3d  33213  bnj570  35528  dfon2lem6  36530  broutsideof2  36867  outsideoftr  36874  outsideofeq  36875  elicc3  37085  nn0prpwlem  37090  nndivsub  37225  fvineqsneu  38314  fvineqsneq  38315  ftc1anc  38599  cntotbnd  38710  heiborlem6  38730  pridlc3  38987  erimeq2  39675  leat2  40331  cvrexchlem  40456  cvratlem  40458  3dim2  40505  ps-2  40515  lncvrelatN  40818  osumcllem11N  41003  relpmin  45920  2reuimp0  48153  iccpartgt  48478  odz2prm2pw  48617  bgoldbachlt  48880  tgblthelfgott  48882  tgoldbach  48884  grimco  48956  isubgr3stgrlem6  49038  isubgr3stgrlem8  49040  uspgrlimlem2  49056  clnbgr3stgrgrlic  49087  gpgedgvtx0  49128  gpgedgvtx1  49129