Theorem imp32 423

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 415	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 411	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp42  431  impr  459  anasss  471  an13s  663  3expb  1136  reuss2  4287  reupick  4290  po2nr  5584  tz7.7  6387  ordtr2  6407  fvmptt  7011  fliftfund  7312  isomin  7336  f1ocnv2d  7664  onint  7788  resf1extb  7930  soseq  8154  tz7.48lem  8427  oalimcl  8544  oaass  8545  omass  8564  omabs  8636  finsschain  9315  frmin  9720  infxpenlem  9996  axcc3  10421  zorn2lem7  10485  addclpi  10876  addnidpi  10885  genpnnp  10989  genpnmax  10991  mulclprlem  11003  dedekindle  11373  prodgt0  12061  ltsubrp  13053  ltaddrp  13054  pfxccat3  14770  sumeven  16444  sumodd  16445  lcmfunsnlem2lem1  16695  divgcdcoprm0  16722  infpnlem1  16969  prmgaplem4  17113  iscatd  17728  imasmnd2  18831  imasgrp2  19120  cyccom  19273  imasrng  20254  imasring  20411  funcrngcsetcALT  20725  mplcoe5lem  22158  dmatmul  22622  scmatmulcl  22643  scmatsgrp1  22647  smatvscl  22649  cpmatacl  22841  cpmatmcllem  22843  0ntr  23196  clsndisj  23200  innei  23250  islpi  23274  tgcnp  23378  haust1  23477  alexsublem  24169  alexsubb  24171  isxmetd  24451  bddiblnc  25969  2lgslem1a1  27518  nodense  27821  precsexlem11  28375  bdaypw2n0bndlem  28621  axcontlem4  29257  ewlkle  29895  clwwlkf  30338  clwwlknonwwlknonb  30397  uhgr3cyclexlem  30472  numclwwlk1lem2foa  30645  grpoidinvlem3  30798  elspansn5  31866  5oalem6  31951  mdi  32587  dmdi  32594  dmdsl3  32607  atom1d  32645  cvexchlem  32660  atcvatlem  32677  chirredlem3  32684  mdsymlem5  32699  f1o3d  32911  bnj570  35237  dfon2lem6  36176  broutsideof2  36512  outsideoftr  36519  outsideofeq  36520  elicc3  36716  nn0prpwlem  36721  nndivsub  36856  fvineqsneu  37944  fvineqsneq  37945  ftc1anc  38239  cntotbnd  38334  heiborlem6  38354  pridlc3  38611  erimeq2  39301  leat2  39957  cvrexchlem  40082  cvratlem  40084  3dim2  40131  ps-2  40141  lncvrelatN  40444  osumcllem11N  40629  relpmin  45552  2reuimp0  47739  iccpartgt  48064  odz2prm2pw  48203  bgoldbachlt  48466  tgblthelfgott  48468  tgoldbach  48470  grimco  48542  isubgr3stgrlem6  48624  isubgr3stgrlem8  48626  uspgrlimlem2  48642  clnbgr3stgrgrlic  48673  gpgedgvtx0  48714  gpgedgvtx1  48715