Theorem imp32 411

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  imp42  419  impr  447  anasss  459  an13s  638  3expb  1100  reuss2  4170  reupick  4174  po2nr  5339  tz7.7  6055  ordtr2  6073  fvmptt  6614  fliftfund  6889  isomin  6913  f1ocnv2d  7216  onint  7326  tz7.48lem  7880  oalimcl  7987  oaass  7988  omass  8007  omabs  8074  finsschain  8626  infxpenlem  9233  axcc3  9658  zorn2lem7  9722  addclpi  10112  addnidpi  10121  genpnnp  10225  genpnmax  10227  mulclprlem  10239  dedekindle  10604  prodgt0  11288  ltsubrp  12242  ltaddrp  12243  swrdccatin1  13924  pfxccat3  13936  swrdccat3OLD  13937  sumeven  15598  sumodd  15599  lcmfunsnlem2lem1  15838  divgcdcoprm0  15865  infpnlem1  16102  prmgaplem4  16246  iscatd  16802  imasmnd2  17795  imasgrp2  18001  imasring  19092  mplcoe5lem  19961  dmatmul  20810  scmatmulcl  20831  scmatsgrp1  20835  smatvscl  20837  cpmatacl  21028  cpmatmcllem  21030  0ntr  21383  clsndisj  21387  innei  21437  islpi  21461  tgcnp  21565  haust1  21664  alexsublem  22356  alexsubb  22358  isxmetd  22639  2lgslem1a1  25667  axcontlem4  26456  ewlkle  27090  clwwlkfOLD  27564  clwwlkf  27569  clwwlknonwwlknonb  27634  uhgr3cyclexlem  27710  numclwwlk1lem2foa  27895  numclwwlk1lem2foaOLD  27896  grpoidinvlem3  28060  elspansn5  29132  5oalem6  29217  mdi  29853  dmdi  29860  dmdsl3  29873  atom1d  29911  cvexchlem  29926  atcvatlem  29943  chirredlem3  29950  mdsymlem5  29965  f1o3d  30136  bnj570  31830  dfon2lem6  32559  frmin  32611  soseq  32623  nodense  32723  broutsideof2  33110  outsideoftr  33117  outsideofeq  33118  elicc3  33192  nn0prpwlem  33197  nndivsub  33331  fvineqsneu  34139  fvineqsneq  34140  bddiblnc  34409  ftc1anc  34422  cntotbnd  34522  heiborlem6  34542  pridlc3  34799  erim2  35362  leat2  35881  cvrexchlem  36006  cvratlem  36008  3dim2  36055  ps-2  36065  lncvrelatN  36368  osumcllem11N  36553  2reuimp0  42725  iccpartgt  42965  odz2prm2pw  43099  bgoldbachlt  43352  tgblthelfgott  43354  tgoldbach  43356  isomgrsym  43375  isomgrtr  43378  funcrngcsetcALT  43640