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  4255  reupick  4258  po2nr  5517  tz7.7  6290  ordtr2  6308  fvmptt  6890  fliftfund  7178  isomin  7202  f1ocnv2d  7514  onint  7632  tz7.48lem  8261  oalimcl  8374  oaass  8375  omass  8394  omabs  8462  finsschain  9102  frmin  9505  frminOLD  9506  infxpenlem  9768  axcc3  10193  zorn2lem7  10257  addclpi  10647  addnidpi  10656  genpnnp  10760  genpnmax  10762  mulclprlem  10774  dedekindle  11137  prodgt0  11820  ltsubrp  12763  ltaddrp  12764  pfxccat3  14443  sumeven  16092  sumodd  16093  lcmfunsnlem2lem1  16339  divgcdcoprm0  16366  infpnlem1  16607  prmgaplem4  16751  iscatd  17378  imasmnd2  18418  imasgrp2  18686  cyccom  18818  imasring  19854  mplcoe5lem  21236  dmatmul  21642  scmatmulcl  21663  scmatsgrp1  21667  smatvscl  21669  cpmatacl  21861  cpmatmcllem  21863  0ntr  22218  clsndisj  22222  innei  22272  islpi  22296  tgcnp  22400  haust1  22499  alexsublem  23191  alexsubb  23193  isxmetd  23475  bddiblnc  25002  2lgslem1a1  26533  axcontlem4  27331  ewlkle  27968  clwwlkf  28405  clwwlknonwwlknonb  28464  uhgr3cyclexlem  28539  numclwwlk1lem2foa  28712  grpoidinvlem3  28862  elspansn5  29930  5oalem6  30015  mdi  30651  dmdi  30658  dmdsl3  30671  atom1d  30709  cvexchlem  30724  atcvatlem  30741  chirredlem3  30748  mdsymlem5  30763  f1o3d  30956  bnj570  32879  dfon2lem6  33758  soseq  33797  nodense  33889  broutsideof2  34418  outsideoftr  34425  outsideofeq  34426  elicc3  34500  nn0prpwlem  34505  nndivsub  34640  fvineqsneu  35576  fvineqsneq  35577  ftc1anc  35852  cntotbnd  35948  heiborlem6  35968  pridlc3  36225  erim2  36783  leat2  37302  cvrexchlem  37427  cvratlem  37429  3dim2  37476  ps-2  37486  lncvrelatN  37789  osumcllem11N  37974  2reuimp0  44572  iccpartgt  44846  odz2prm2pw  44982  bgoldbachlt  45232  tgblthelfgott  45234  tgoldbach  45236  isomgrsym  45255  isomgrtr  45258  funcrngcsetcALT  45524