Theorem imp32 449

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp32	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		impd.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 447	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 445	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  imp42  620  impr  649  anasss  679  an13s  845  3expb  1266  reuss2  3907  reupick  3911  po2nr  5048  tz7.7  5749  ordtr2  5768  fvmptt  6300  fliftfund  6563  isomin  6587  f1ocnv2d  6886  onint  6995  tz7.48lem  7536  oalimcl  7640  oaass  7641  omass  7660  omabs  7727  finsschain  8273  infxpenlem  8836  axcc3  9260  zorn2lem7  9324  addclpi  9714  addnidpi  9723  genpnnp  9827  genpnmax  9829  mulclprlem  9841  dedekindle  10201  prodgt0  10868  ltsubrp  11866  ltaddrp  11867  swrdccatin1  13483  swrdccat3  13492  sumeven  15110  sumodd  15111  lcmfunsnlem2lem1  15351  divgcdcoprm0  15379  infpnlem1  15614  prmgaplem4  15758  iscatd  16334  imasmnd2  17327  imasgrp2  17530  imasring  18619  mplcoe5lem  19467  dmatmul  20303  scmatmulcl  20324  scmatsgrp1  20328  smatvscl  20330  cpmatacl  20521  cpmatmcllem  20523  0ntr  20875  clsndisj  20879  innei  20929  islpi  20953  tgcnp  21057  haust1  21156  alexsublem  21848  alexsubb  21850  isxmetd  22131  2lgslem1a1  25114  axcontlem4  25847  ewlkle  26501  wlkwwlksur  26783  clwwlksf  26915  uhgr3cyclexlem  27041  clwwlkextfrlem1  27208  grpoidinvlem3  27360  elspansn5  28433  5oalem6  28518  mdi  29154  dmdi  29161  dmdsl3  29174  atom1d  29212  cvexchlem  29227  atcvatlem  29244  chirredlem3  29251  mdsymlem5  29266  f1o3d  29431  bnj570  30975  dfon2lem6  31693  frmin  31739  soseq  31751  nodense  31842  broutsideof2  32229  outsideoftr  32236  outsideofeq  32237  elicc3  32311  nn0prpwlem  32317  nndivsub  32456  bddiblnc  33480  ftc1anc  33493  cntotbnd  33595  heiborlem6  33615  pridlc3  33872  leat2  34581  cvrexchlem  34705  cvratlem  34707  3dim2  34754  ps-2  34764  lncvrelatN  35067  osumcllem11N  35252  iccpartgt  41363  pfxccat3  41426  odz2prm2pw  41475  bgoldbachlt  41701  tgblthelfgott  41703  tgoldbach  41705  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  tgoldbachOLD  41712  funcrngcsetcALT  41999