Theorem imp32 419

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  imp42  427  impr  455  anasss  467  an13s  648  3expb  1119  reuss2  4250  reupick  4253  po2nr  5518  tz7.7  6296  ordtr2  6314  fvmptt  6904  fliftfund  7193  isomin  7217  f1ocnv2d  7531  onint  7649  tz7.48lem  8281  oalimcl  8400  oaass  8401  omass  8420  omabs  8490  finsschain  9135  frmin  9516  infxpenlem  9778  axcc3  10203  zorn2lem7  10267  addclpi  10657  addnidpi  10666  genpnnp  10770  genpnmax  10772  mulclprlem  10784  dedekindle  11148  prodgt0  11831  ltsubrp  12775  ltaddrp  12776  pfxccat3  14456  sumeven  16105  sumodd  16106  lcmfunsnlem2lem1  16352  divgcdcoprm0  16379  infpnlem1  16620  prmgaplem4  16764  iscatd  17391  imasmnd2  18431  imasgrp2  18699  cyccom  18831  imasring  19867  mplcoe5lem  21249  dmatmul  21655  scmatmulcl  21676  scmatsgrp1  21680  smatvscl  21682  cpmatacl  21874  cpmatmcllem  21876  0ntr  22231  clsndisj  22235  innei  22285  islpi  22309  tgcnp  22413  haust1  22512  alexsublem  23204  alexsubb  23206  isxmetd  23488  bddiblnc  25015  2lgslem1a1  26546  axcontlem4  27344  ewlkle  27981  clwwlkf  28420  clwwlknonwwlknonb  28479  uhgr3cyclexlem  28554  numclwwlk1lem2foa  28727  grpoidinvlem3  28877  elspansn5  29945  5oalem6  30030  mdi  30666  dmdi  30673  dmdsl3  30686  atom1d  30724  cvexchlem  30739  atcvatlem  30756  chirredlem3  30763  mdsymlem5  30778  f1o3d  30971  bnj570  32894  dfon2lem6  33773  soseq  33812  nodense  33904  broutsideof2  34433  outsideoftr  34440  outsideofeq  34441  elicc3  34515  nn0prpwlem  34520  nndivsub  34655  fvineqsneu  35591  fvineqsneq  35592  ftc1anc  35867  cntotbnd  35963  heiborlem6  35983  pridlc3  36240  erim2  36796  leat2  37315  cvrexchlem  37440  cvratlem  37442  3dim2  37489  ps-2  37499  lncvrelatN  37802  osumcllem11N  37987  2reuimp0  44617  iccpartgt  44890  odz2prm2pw  45026  bgoldbachlt  45276  tgblthelfgott  45278  tgoldbach  45280  isomgrsym  45299  isomgrtr  45302  funcrngcsetcALT  45568