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  5577  tz7.7  6383  ordtr2  6403  fvmptt  7007  fliftfund  7314  isomin  7338  f1ocnv2d  7667  onint  7789  resf1extb  7931  soseq  8157  tz7.48lem  8430  oalimcl  8547  oaass  8548  omass  8567  omabs  8639  finsschain  9326  frmin  9731  infxpenlem  10016  axcc3  10440  zorn2lem7  10504  addclpi  10901  addnidpi  10910  genpnnp  11014  genpnmax  11016  mulclprlem  11028  dedekindle  11398  prodgt0  12086  ltsubrp  13080  ltaddrp  13081  pfxccat3  14803  sumeven  16477  sumodd  16478  lcmfunsnlem2lem1  16728  divgcdcoprm0  16755  infpnlem1  17002  prmgaplem4  17146  iscatd  17761  mgmn0plusgf  18741  imasmnd2  18881  imasgrp2  19178  cyccom  19331  imasrng  20312  imasring  20471  funcrngcsetcALT  20803  cmprmidlmcl  21538  mplcoe5lem  22255  dmatmul  22719  scmatmulcl  22740  scmatsgrp1  22744  smatvscl  22746  cpmatacl  22941  cpmatmcllem  22943  0ntr  23296  clsndisj  23300  innei  23350  islpi  23374  tgcnp  23478  haust1  23577  alexsublem  24270  alexsubb  24272  isxmetd  24552  bddiblnc  26069  2lgslem1a1  27625  nodense  27928  precsexlem11  28482  bdaypw2n0bndlem  28728  axcontlem4  29424  ewlkle  30065  clwwlkf  30517  clwwlknonwwlknonb  30576  uhgr3cyclexlem  30661  numclwwlk1lem2foa  30834  grpoidinvlem3  30987  elspansn5  32055  5oalem6  32140  mdi  32776  dmdi  32783  dmdsl3  32796  atom1d  32834  cvexchlem  32849  atcvatlem  32866  chirredlem3  32873  mdsymlem5  32888  f1o3d  33099  bnj570  35414  dfon2lem6  36365  broutsideof2  36702  outsideoftr  36709  outsideofeq  36710  elicc3  36936  nn0prpwlem  36941  nndivsub  37076  fvineqsneu  38165  fvineqsneq  38166  ftc1anc  38450  cntotbnd  38546  heiborlem6  38566  pridlc3  38823  erimeq2  39511  leat2  40167  cvrexchlem  40292  cvratlem  40294  3dim2  40341  ps-2  40351  lncvrelatN  40654  osumcllem11N  40839  relpmin  45775  2reuimp0  48002  iccpartgt  48327  odz2prm2pw  48466  bgoldbachlt  48729  tgblthelfgott  48731  tgoldbach  48733  grimco  48805  isubgr3stgrlem6  48887  isubgr3stgrlem8  48889  uspgrlimlem2  48905  clnbgr3stgrgrlic  48936  gpgedgvtx0  48977  gpgedgvtx1  48978