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  650  3expb  1120  reuss2  4345  reupick  4348  po2nr  5622  tz7.7  6421  ordtr2  6439  fvmptt  7049  fliftfund  7349  isomin  7373  f1ocnv2d  7703  onint  7826  soseq  8200  tz7.48lem  8497  oalimcl  8616  oaass  8617  omass  8636  omabs  8707  finsschain  9429  frmin  9818  infxpenlem  10082  axcc3  10507  zorn2lem7  10571  addclpi  10961  addnidpi  10970  genpnnp  11074  genpnmax  11076  mulclprlem  11088  dedekindle  11454  prodgt0  12141  ltsubrp  13093  ltaddrp  13094  pfxccat3  14782  sumeven  16435  sumodd  16436  lcmfunsnlem2lem1  16685  divgcdcoprm0  16712  infpnlem1  16957  prmgaplem4  17101  iscatd  17731  imasmnd2  18809  imasgrp2  19095  cyccom  19243  imasrng  20204  imasring  20353  funcrngcsetcALT  20663  mplcoe5lem  22080  dmatmul  22524  scmatmulcl  22545  scmatsgrp1  22549  smatvscl  22551  cpmatacl  22743  cpmatmcllem  22745  0ntr  23100  clsndisj  23104  innei  23154  islpi  23178  tgcnp  23282  haust1  23381  alexsublem  24073  alexsubb  24075  isxmetd  24357  bddiblnc  25897  2lgslem1a1  27451  nodense  27755  precsexlem11  28259  axcontlem4  29000  ewlkle  29641  clwwlkf  30079  clwwlknonwwlknonb  30138  uhgr3cyclexlem  30213  numclwwlk1lem2foa  30386  grpoidinvlem3  30538  elspansn5  31606  5oalem6  31691  mdi  32327  dmdi  32334  dmdsl3  32347  atom1d  32385  cvexchlem  32400  atcvatlem  32417  chirredlem3  32424  mdsymlem5  32439  f1o3d  32646  bnj570  34881  dfon2lem6  35752  broutsideof2  36086  outsideoftr  36093  outsideofeq  36094  elicc3  36283  nn0prpwlem  36288  nndivsub  36423  fvineqsneu  37377  fvineqsneq  37378  ftc1anc  37661  cntotbnd  37756  heiborlem6  37776  pridlc3  38033  erimeq2  38634  leat2  39250  cvrexchlem  39376  cvratlem  39378  3dim2  39425  ps-2  39435  lncvrelatN  39738  osumcllem11N  39923  2reuimp0  47029  iccpartgt  47301  odz2prm2pw  47437  bgoldbachlt  47687  tgblthelfgott  47689  tgoldbach  47691  grimco  47764  uspgrlimlem2  47813