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

This theorem is referenced by:  imp42  426  impr  454  anasss  466  an13s  651  3expb  1120  reuss2  4276  reupick  4279  po2nr  5544  tz7.7  6341  ordtr2  6360  fvmptt  6959  fliftfund  7257  isomin  7281  f1ocnv2d  7609  onint  7733  resf1extb  7874  soseq  8099  tz7.48lem  8370  oalimcl  8485  oaass  8486  omass  8505  omabs  8577  finsschain  9257  frmin  9659  infxpenlem  9921  axcc3  10346  zorn2lem7  10410  addclpi  10801  addnidpi  10810  genpnnp  10914  genpnmax  10916  mulclprlem  10928  dedekindle  11295  prodgt0  11986  ltsubrp  12941  ltaddrp  12942  pfxccat3  14655  sumeven  16312  sumodd  16313  lcmfunsnlem2lem1  16563  divgcdcoprm0  16590  infpnlem1  16836  prmgaplem4  16980  iscatd  17594  imasmnd2  18697  imasgrp2  18983  cyccom  19130  imasrng  20110  imasring  20264  funcrngcsetcALT  20572  mplcoe5lem  21992  dmatmul  22439  scmatmulcl  22460  scmatsgrp1  22464  smatvscl  22466  cpmatacl  22658  cpmatmcllem  22660  0ntr  23013  clsndisj  23017  innei  23067  islpi  23091  tgcnp  23195  haust1  23294  alexsublem  23986  alexsubb  23988  isxmetd  24268  bddiblnc  25797  2lgslem1a1  27354  nodense  27658  precsexlem11  28185  bdaypw2n0s  28420  axcontlem4  28989  ewlkle  29628  clwwlkf  30071  clwwlknonwwlknonb  30130  uhgr3cyclexlem  30205  numclwwlk1lem2foa  30378  grpoidinvlem3  30530  elspansn5  31598  5oalem6  31683  mdi  32319  dmdi  32326  dmdsl3  32339  atom1d  32377  cvexchlem  32392  atcvatlem  32409  chirredlem3  32416  mdsymlem5  32431  f1o3d  32653  bnj570  35010  dfon2lem6  35929  broutsideof2  36265  outsideoftr  36272  outsideofeq  36273  elicc3  36460  nn0prpwlem  36465  nndivsub  36600  fvineqsneu  37555  fvineqsneq  37556  ftc1anc  37841  cntotbnd  37936  heiborlem6  37956  pridlc3  38213  erimeq2  38876  leat2  39493  cvrexchlem  39618  cvratlem  39620  3dim2  39667  ps-2  39677  lncvrelatN  39980  osumcllem11N  40165  relpmin  45135  2reuimp0  47302  iccpartgt  47615  odz2prm2pw  47751  bgoldbachlt  48001  tgblthelfgott  48003  tgoldbach  48005  grimco  48077  isubgr3stgrlem6  48159  isubgr3stgrlem8  48161  uspgrlimlem2  48177  clnbgr3stgrgrlic  48208  gpgedgvtx0  48249  gpgedgvtx1  48250