Theorem imp32 421

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imp42  429  impr  457  anasss  469  an13s  649  3expb  1116  reuss2  4283  reupick  4287  po2nr  5487  tz7.7  6217  ordtr2  6235  fvmptt  6788  fliftfund  7066  isomin  7090  f1ocnv2d  7398  onint  7510  tz7.48lem  8077  oalimcl  8186  oaass  8187  omass  8206  omabs  8274  finsschain  8831  infxpenlem  9439  axcc3  9860  zorn2lem7  9924  addclpi  10314  addnidpi  10323  genpnnp  10427  genpnmax  10429  mulclprlem  10441  dedekindle  10804  prodgt0  11487  ltsubrp  12426  ltaddrp  12427  pfxccat3  14096  sumeven  15738  sumodd  15739  lcmfunsnlem2lem1  15982  divgcdcoprm0  16009  infpnlem1  16246  prmgaplem4  16390  iscatd  16944  imasmnd2  17948  imasgrp2  18214  cyccom  18346  imasring  19369  mplcoe5lem  20248  dmatmul  21106  scmatmulcl  21127  scmatsgrp1  21131  smatvscl  21133  cpmatacl  21324  cpmatmcllem  21326  0ntr  21679  clsndisj  21683  innei  21733  islpi  21757  tgcnp  21861  haust1  21960  alexsublem  22652  alexsubb  22654  isxmetd  22936  2lgslem1a1  25965  axcontlem4  26753  ewlkle  27387  clwwlkf  27826  clwwlknonwwlknonb  27885  uhgr3cyclexlem  27960  numclwwlk1lem2foa  28133  grpoidinvlem3  28283  elspansn5  29351  5oalem6  29436  mdi  30072  dmdi  30079  dmdsl3  30092  atom1d  30130  cvexchlem  30145  atcvatlem  30162  chirredlem3  30169  mdsymlem5  30184  f1o3d  30372  bnj570  32177  dfon2lem6  33033  frmin  33084  soseq  33096  nodense  33196  broutsideof2  33583  outsideoftr  33590  outsideofeq  33591  elicc3  33665  nn0prpwlem  33670  nndivsub  33805  fvineqsneu  34695  fvineqsneq  34696  bddiblnc  34977  ftc1anc  34990  cntotbnd  35089  heiborlem6  35109  pridlc3  35366  erim2  35926  leat2  36445  cvrexchlem  36570  cvratlem  36572  3dim2  36619  ps-2  36629  lncvrelatN  36932  osumcllem11N  37117  2reuimp0  43333  iccpartgt  43607  odz2prm2pw  43745  bgoldbachlt  43998  tgblthelfgott  44000  tgoldbach  44002  isomgrsym  44021  isomgrtr  44024  funcrngcsetcALT  44290