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  4273  reupick  4276  po2nr  5536  tz7.7  6332  ordtr2  6351  fvmptt  6949  fliftfund  7247  isomin  7271  f1ocnv2d  7599  onint  7723  resf1extb  7864  soseq  8089  tz7.48lem  8360  oalimcl  8475  oaass  8476  omass  8495  omabs  8566  finsschain  9243  frmin  9642  infxpenlem  9904  axcc3  10329  zorn2lem7  10393  addclpi  10783  addnidpi  10792  genpnnp  10896  genpnmax  10898  mulclprlem  10910  dedekindle  11277  prodgt0  11968  ltsubrp  12928  ltaddrp  12929  pfxccat3  14641  sumeven  16298  sumodd  16299  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  infpnlem1  16822  prmgaplem4  16966  iscatd  17579  imasmnd2  18682  imasgrp2  18968  cyccom  19115  imasrng  20095  imasring  20248  funcrngcsetcALT  20556  mplcoe5lem  21974  dmatmul  22412  scmatmulcl  22433  scmatsgrp1  22437  smatvscl  22439  cpmatacl  22631  cpmatmcllem  22633  0ntr  22986  clsndisj  22990  innei  23040  islpi  23064  tgcnp  23168  haust1  23267  alexsublem  23959  alexsubb  23961  isxmetd  24241  bddiblnc  25770  2lgslem1a1  27327  nodense  27631  precsexlem11  28155  axcontlem4  28945  ewlkle  29584  clwwlkf  30027  clwwlknonwwlknonb  30086  uhgr3cyclexlem  30161  numclwwlk1lem2foa  30334  grpoidinvlem3  30486  elspansn5  31554  5oalem6  31639  mdi  32275  dmdi  32282  dmdsl3  32295  atom1d  32333  cvexchlem  32348  atcvatlem  32365  chirredlem3  32372  mdsymlem5  32387  f1o3d  32608  bnj570  34917  dfon2lem6  35830  broutsideof2  36166  outsideoftr  36173  outsideofeq  36174  elicc3  36361  nn0prpwlem  36366  nndivsub  36501  fvineqsneu  37455  fvineqsneq  37456  ftc1anc  37751  cntotbnd  37846  heiborlem6  37866  pridlc3  38123  erimeq2  38786  leat2  39403  cvrexchlem  39528  cvratlem  39530  3dim2  39577  ps-2  39587  lncvrelatN  39890  osumcllem11N  40075  relpmin  45055  2reuimp0  47224  iccpartgt  47537  odz2prm2pw  47673  bgoldbachlt  47923  tgblthelfgott  47925  tgoldbach  47927  grimco  47999  isubgr3stgrlem6  48081  isubgr3stgrlem8  48083  uspgrlimlem2  48099  clnbgr3stgrgrlic  48130  gpgedgvtx0  48171  gpgedgvtx1  48172