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  4292  reupick  4295  po2nr  5563  tz7.7  6361  ordtr2  6380  fvmptt  6991  fliftfund  7291  isomin  7315  f1ocnv2d  7645  onint  7769  resf1extb  7913  soseq  8141  tz7.48lem  8412  oalimcl  8527  oaass  8528  omass  8547  omabs  8618  finsschain  9317  frmin  9709  infxpenlem  9973  axcc3  10398  zorn2lem7  10462  addclpi  10852  addnidpi  10861  genpnnp  10965  genpnmax  10967  mulclprlem  10979  dedekindle  11345  prodgt0  12036  ltsubrp  12996  ltaddrp  12997  pfxccat3  14706  sumeven  16364  sumodd  16365  lcmfunsnlem2lem1  16615  divgcdcoprm0  16642  infpnlem1  16888  prmgaplem4  17032  iscatd  17641  imasmnd2  18708  imasgrp2  18994  cyccom  19142  imasrng  20093  imasring  20246  funcrngcsetcALT  20557  mplcoe5lem  21953  dmatmul  22391  scmatmulcl  22412  scmatsgrp1  22416  smatvscl  22418  cpmatacl  22610  cpmatmcllem  22612  0ntr  22965  clsndisj  22969  innei  23019  islpi  23043  tgcnp  23147  haust1  23246  alexsublem  23938  alexsubb  23940  isxmetd  24221  bddiblnc  25750  2lgslem1a1  27307  nodense  27611  precsexlem11  28126  axcontlem4  28901  ewlkle  29540  clwwlkf  29983  clwwlknonwwlknonb  30042  uhgr3cyclexlem  30117  numclwwlk1lem2foa  30290  grpoidinvlem3  30442  elspansn5  31510  5oalem6  31595  mdi  32231  dmdi  32238  dmdsl3  32251  atom1d  32289  cvexchlem  32304  atcvatlem  32321  chirredlem3  32328  mdsymlem5  32343  f1o3d  32558  bnj570  34902  dfon2lem6  35783  broutsideof2  36117  outsideoftr  36124  outsideofeq  36125  elicc3  36312  nn0prpwlem  36317  nndivsub  36452  fvineqsneu  37406  fvineqsneq  37407  ftc1anc  37702  cntotbnd  37797  heiborlem6  37817  pridlc3  38074  erimeq2  38677  leat2  39294  cvrexchlem  39420  cvratlem  39422  3dim2  39469  ps-2  39479  lncvrelatN  39782  osumcllem11N  39967  relpmin  44949  2reuimp0  47119  iccpartgt  47432  odz2prm2pw  47568  bgoldbachlt  47818  tgblthelfgott  47820  tgoldbach  47822  grimco  47893  isubgr3stgrlem6  47974  isubgr3stgrlem8  47976  uspgrlimlem2  47992  clnbgr3stgrgrlic  48015  gpgedgvtx0  48056  gpgedgvtx1  48057