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  652  3expb  1121  reuss2  4267  reupick  4270  po2nr  5547  tz7.7  6344  ordtr2  6363  fvmptt  6963  fliftfund  7262  isomin  7286  f1ocnv2d  7614  onint  7738  resf1extb  7879  soseq  8103  tz7.48lem  8374  oalimcl  8489  oaass  8490  omass  8509  omabs  8581  finsschain  9263  frmin  9667  infxpenlem  9929  axcc3  10354  zorn2lem7  10418  addclpi  10809  addnidpi  10818  genpnnp  10922  genpnmax  10924  mulclprlem  10936  dedekindle  11304  prodgt0  11996  ltsubrp  12974  ltaddrp  12975  pfxccat3  14690  sumeven  16350  sumodd  16351  lcmfunsnlem2lem1  16601  divgcdcoprm0  16628  infpnlem1  16875  prmgaplem4  17019  iscatd  17633  imasmnd2  18736  imasgrp2  19025  cyccom  19172  imasrng  20152  imasring  20304  funcrngcsetcALT  20612  mplcoe5lem  22030  dmatmul  22475  scmatmulcl  22496  scmatsgrp1  22500  smatvscl  22502  cpmatacl  22694  cpmatmcllem  22696  0ntr  23049  clsndisj  23053  innei  23103  islpi  23127  tgcnp  23231  haust1  23330  alexsublem  24022  alexsubb  24024  isxmetd  24304  bddiblnc  25822  2lgslem1a1  27369  nodense  27673  precsexlem11  28226  bdaypw2n0bndlem  28472  axcontlem4  29053  ewlkle  29692  clwwlkf  30135  clwwlknonwwlknonb  30194  uhgr3cyclexlem  30269  numclwwlk1lem2foa  30442  grpoidinvlem3  30595  elspansn5  31663  5oalem6  31748  mdi  32384  dmdi  32391  dmdsl3  32404  atom1d  32442  cvexchlem  32457  atcvatlem  32474  chirredlem3  32481  mdsymlem5  32496  f1o3d  32717  bnj570  35066  dfon2lem6  35987  broutsideof2  36323  outsideoftr  36330  outsideofeq  36331  elicc3  36518  nn0prpwlem  36523  nndivsub  36658  fvineqsneu  37744  fvineqsneq  37745  ftc1anc  38039  cntotbnd  38134  heiborlem6  38154  pridlc3  38411  erimeq2  39101  leat2  39757  cvrexchlem  39882  cvratlem  39884  3dim2  39931  ps-2  39941  lncvrelatN  40244  osumcllem11N  40429  relpmin  45400  2reuimp0  47577  iccpartgt  47902  odz2prm2pw  48041  bgoldbachlt  48304  tgblthelfgott  48306  tgoldbach  48308  grimco  48380  isubgr3stgrlem6  48462  isubgr3stgrlem8  48464  uspgrlimlem2  48480  clnbgr3stgrgrlic  48511  gpgedgvtx0  48552  gpgedgvtx1  48553