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  4279  reupick  4282  po2nr  5585  tz7.7  6390  ordtr2  6410  fvmptt  7014  fliftfund  7320  isomin  7344  f1ocnv2d  7673  onint  7795  resf1extb  7937  soseq  8161  tz7.48lem  8434  oalimcl  8551  oaass  8552  omass  8571  omabs  8643  finsschain  9323  frmin  9728  infxpenlem  10013  axcc3  10437  zorn2lem7  10501  addclpi  10892  addnidpi  10901  genpnnp  11005  genpnmax  11007  mulclprlem  11019  dedekindle  11389  prodgt0  12077  ltsubrp  13070  ltaddrp  13071  pfxccat3  14793  sumeven  16467  sumodd  16468  lcmfunsnlem2lem1  16718  divgcdcoprm0  16745  infpnlem1  16992  prmgaplem4  17136  iscatd  17751  mgmn0plusgf  18731  imasmnd2  18869  imasgrp2  19165  cyccom  19318  imasrng  20299  imasring  20458  funcrngcsetcALT  20790  cmprmidlmcl  21525  mplcoe5lem  22240  dmatmul  22704  scmatmulcl  22725  scmatsgrp1  22729  smatvscl  22731  cpmatacl  22923  cpmatmcllem  22925  0ntr  23278  clsndisj  23282  innei  23332  islpi  23356  tgcnp  23460  haust1  23559  alexsublem  24252  alexsubb  24254  isxmetd  24534  bddiblnc  26052  2lgslem1a1  27604  nodense  27907  precsexlem11  28461  bdaypw2n0bndlem  28707  axcontlem4  29372  ewlkle  30013  clwwlkf  30465  clwwlknonwwlknonb  30524  uhgr3cyclexlem  30603  numclwwlk1lem2foa  30776  grpoidinvlem3  30929  elspansn5  31997  5oalem6  32082  mdi  32718  dmdi  32725  dmdsl3  32738  atom1d  32776  cvexchlem  32791  atcvatlem  32808  chirredlem3  32815  mdsymlem5  32830  f1o3d  33042  bnj570  35358  dfon2lem6  36315  broutsideof2  36651  outsideoftr  36658  outsideofeq  36659  elicc3  36885  nn0prpwlem  36890  nndivsub  37025  fvineqsneu  38114  fvineqsneq  38115  ftc1anc  38409  cntotbnd  38505  heiborlem6  38525  pridlc3  38782  erimeq2  39470  leat2  40126  cvrexchlem  40251  cvratlem  40253  3dim2  40300  ps-2  40310  lncvrelatN  40613  osumcllem11N  40798  relpmin  45719  2reuimp0  47909  iccpartgt  48234  odz2prm2pw  48373  bgoldbachlt  48636  tgblthelfgott  48638  tgoldbach  48640  grimco  48712  isubgr3stgrlem6  48794  isubgr3stgrlem8  48796  uspgrlimlem2  48812  clnbgr3stgrgrlic  48843  gpgedgvtx0  48884  gpgedgvtx1  48885