Theorem imp32 418

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  imp42  426  impr  454  anasss  466  an13s  647  3expb  1118  reuss2  4246  reupick  4249  po2nr  5508  tz7.7  6277  ordtr2  6295  fvmptt  6877  fliftfund  7164  isomin  7188  f1ocnv2d  7500  onint  7617  tz7.48lem  8242  oalimcl  8353  oaass  8354  omass  8373  omabs  8441  finsschain  9056  frmin  9438  infxpenlem  9700  axcc3  10125  zorn2lem7  10189  addclpi  10579  addnidpi  10588  genpnnp  10692  genpnmax  10694  mulclprlem  10706  dedekindle  11069  prodgt0  11752  ltsubrp  12695  ltaddrp  12696  pfxccat3  14375  sumeven  16024  sumodd  16025  lcmfunsnlem2lem1  16271  divgcdcoprm0  16298  infpnlem1  16539  prmgaplem4  16683  iscatd  17299  imasmnd2  18337  imasgrp2  18605  cyccom  18737  imasring  19773  mplcoe5lem  21150  dmatmul  21554  scmatmulcl  21575  scmatsgrp1  21579  smatvscl  21581  cpmatacl  21773  cpmatmcllem  21775  0ntr  22130  clsndisj  22134  innei  22184  islpi  22208  tgcnp  22312  haust1  22411  alexsublem  23103  alexsubb  23105  isxmetd  23387  bddiblnc  24911  2lgslem1a1  26442  axcontlem4  27238  ewlkle  27875  clwwlkf  28312  clwwlknonwwlknonb  28371  uhgr3cyclexlem  28446  numclwwlk1lem2foa  28619  grpoidinvlem3  28769  elspansn5  29837  5oalem6  29922  mdi  30558  dmdi  30565  dmdsl3  30578  atom1d  30616  cvexchlem  30631  atcvatlem  30648  chirredlem3  30655  mdsymlem5  30670  f1o3d  30863  bnj570  32785  dfon2lem6  33670  soseq  33730  nodense  33822  broutsideof2  34351  outsideoftr  34358  outsideofeq  34359  elicc3  34433  nn0prpwlem  34438  nndivsub  34573  fvineqsneu  35509  fvineqsneq  35510  ftc1anc  35785  cntotbnd  35881  heiborlem6  35901  pridlc3  36158  erim2  36716  leat2  37235  cvrexchlem  37360  cvratlem  37362  3dim2  37409  ps-2  37419  lncvrelatN  37722  osumcllem11N  37907  2reuimp0  44493  iccpartgt  44767  odz2prm2pw  44903  bgoldbachlt  45153  tgblthelfgott  45155  tgoldbach  45157  isomgrsym  45176  isomgrtr  45179  funcrngcsetcALT  45445