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  4291  reupick  4294  po2nr  5562  tz7.7  6360  ordtr2  6379  fvmptt  6990  fliftfund  7290  isomin  7314  f1ocnv2d  7644  onint  7768  resf1extb  7912  soseq  8140  tz7.48lem  8411  oalimcl  8526  oaass  8527  omass  8546  omabs  8617  finsschain  9316  frmin  9708  infxpenlem  9972  axcc3  10397  zorn2lem7  10461  addclpi  10851  addnidpi  10860  genpnnp  10964  genpnmax  10966  mulclprlem  10978  dedekindle  11344  prodgt0  12035  ltsubrp  12995  ltaddrp  12996  pfxccat3  14705  sumeven  16363  sumodd  16364  lcmfunsnlem2lem1  16614  divgcdcoprm0  16641  infpnlem1  16887  prmgaplem4  17031  iscatd  17640  imasmnd2  18707  imasgrp2  18993  cyccom  19141  imasrng  20092  imasring  20245  funcrngcsetcALT  20556  mplcoe5lem  21952  dmatmul  22390  scmatmulcl  22411  scmatsgrp1  22415  smatvscl  22417  cpmatacl  22609  cpmatmcllem  22611  0ntr  22964  clsndisj  22968  innei  23018  islpi  23042  tgcnp  23146  haust1  23245  alexsublem  23937  alexsubb  23939  isxmetd  24220  bddiblnc  25749  2lgslem1a1  27306  nodense  27610  precsexlem11  28125  axcontlem4  28900  ewlkle  29539  clwwlkf  29982  clwwlknonwwlknonb  30041  uhgr3cyclexlem  30116  numclwwlk1lem2foa  30289  grpoidinvlem3  30441  elspansn5  31509  5oalem6  31594  mdi  32230  dmdi  32237  dmdsl3  32250  atom1d  32288  cvexchlem  32303  atcvatlem  32320  chirredlem3  32327  mdsymlem5  32342  f1o3d  32557  bnj570  34901  dfon2lem6  35771  broutsideof2  36105  outsideoftr  36112  outsideofeq  36113  elicc3  36300  nn0prpwlem  36305  nndivsub  36440  fvineqsneu  37394  fvineqsneq  37395  ftc1anc  37690  cntotbnd  37785  heiborlem6  37805  pridlc3  38062  erimeq2  38665  leat2  39282  cvrexchlem  39408  cvratlem  39410  3dim2  39457  ps-2  39467  lncvrelatN  39770  osumcllem11N  39955  relpmin  44935  2reuimp0  47105  iccpartgt  47418  odz2prm2pw  47554  bgoldbachlt  47804  tgblthelfgott  47806  tgoldbach  47808  grimco  47879  isubgr3stgrlem6  47960  isubgr3stgrlem8  47962  uspgrlimlem2  47978  clnbgr3stgrgrlic  48001  gpgedgvtx0  48042  gpgedgvtx1  48043