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  4289  reupick  4292  po2nr  5560  tz7.7  6358  ordtr2  6377  fvmptt  6988  fliftfund  7288  isomin  7312  f1ocnv2d  7642  onint  7766  resf1extb  7910  soseq  8138  tz7.48lem  8409  oalimcl  8524  oaass  8525  omass  8544  omabs  8615  finsschain  9310  frmin  9702  infxpenlem  9966  axcc3  10391  zorn2lem7  10455  addclpi  10845  addnidpi  10854  genpnnp  10958  genpnmax  10960  mulclprlem  10972  dedekindle  11338  prodgt0  12029  ltsubrp  12989  ltaddrp  12990  pfxccat3  14699  sumeven  16357  sumodd  16358  lcmfunsnlem2lem1  16608  divgcdcoprm0  16635  infpnlem1  16881  prmgaplem4  17025  iscatd  17634  imasmnd2  18701  imasgrp2  18987  cyccom  19135  imasrng  20086  imasring  20239  funcrngcsetcALT  20550  mplcoe5lem  21946  dmatmul  22384  scmatmulcl  22405  scmatsgrp1  22409  smatvscl  22411  cpmatacl  22603  cpmatmcllem  22605  0ntr  22958  clsndisj  22962  innei  23012  islpi  23036  tgcnp  23140  haust1  23239  alexsublem  23931  alexsubb  23933  isxmetd  24214  bddiblnc  25743  2lgslem1a1  27300  nodense  27604  precsexlem11  28119  axcontlem4  28894  ewlkle  29533  clwwlkf  29976  clwwlknonwwlknonb  30035  uhgr3cyclexlem  30110  numclwwlk1lem2foa  30283  grpoidinvlem3  30435  elspansn5  31503  5oalem6  31588  mdi  32224  dmdi  32231  dmdsl3  32244  atom1d  32282  cvexchlem  32297  atcvatlem  32314  chirredlem3  32321  mdsymlem5  32336  f1o3d  32551  bnj570  34895  dfon2lem6  35776  broutsideof2  36110  outsideoftr  36117  outsideofeq  36118  elicc3  36305  nn0prpwlem  36310  nndivsub  36445  fvineqsneu  37399  fvineqsneq  37400  ftc1anc  37695  cntotbnd  37790  heiborlem6  37810  pridlc3  38067  erimeq2  38670  leat2  39287  cvrexchlem  39413  cvratlem  39415  3dim2  39462  ps-2  39472  lncvrelatN  39775  osumcllem11N  39960  relpmin  44942  2reuimp0  47115  iccpartgt  47428  odz2prm2pw  47564  bgoldbachlt  47814  tgblthelfgott  47816  tgoldbach  47818  grimco  47889  isubgr3stgrlem6  47970  isubgr3stgrlem8  47972  uspgrlimlem2  47988  clnbgr3stgrgrlic  48011  gpgedgvtx0  48052  gpgedgvtx1  48053