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  4277  reupick  4280  po2nr  5541  tz7.7  6333  ordtr2  6352  fvmptt  6950  fliftfund  7250  isomin  7274  f1ocnv2d  7602  onint  7726  resf1extb  7867  soseq  8092  tz7.48lem  8363  oalimcl  8478  oaass  8479  omass  8498  omabs  8569  finsschain  9249  frmin  9645  infxpenlem  9907  axcc3  10332  zorn2lem7  10396  addclpi  10786  addnidpi  10795  genpnnp  10899  genpnmax  10901  mulclprlem  10913  dedekindle  11280  prodgt0  11971  ltsubrp  12931  ltaddrp  12932  pfxccat3  14640  sumeven  16298  sumodd  16299  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  infpnlem1  16822  prmgaplem4  16966  iscatd  17579  imasmnd2  18648  imasgrp2  18934  cyccom  19082  imasrng  20062  imasring  20215  funcrngcsetcALT  20526  mplcoe5lem  21944  dmatmul  22382  scmatmulcl  22403  scmatsgrp1  22407  smatvscl  22409  cpmatacl  22601  cpmatmcllem  22603  0ntr  22956  clsndisj  22960  innei  23010  islpi  23034  tgcnp  23138  haust1  23237  alexsublem  23929  alexsubb  23931  isxmetd  24212  bddiblnc  25741  2lgslem1a1  27298  nodense  27602  precsexlem11  28124  axcontlem4  28912  ewlkle  29551  clwwlkf  29991  clwwlknonwwlknonb  30050  uhgr3cyclexlem  30125  numclwwlk1lem2foa  30298  grpoidinvlem3  30450  elspansn5  31518  5oalem6  31603  mdi  32239  dmdi  32246  dmdsl3  32259  atom1d  32297  cvexchlem  32312  atcvatlem  32329  chirredlem3  32336  mdsymlem5  32351  f1o3d  32569  bnj570  34872  dfon2lem6  35762  broutsideof2  36096  outsideoftr  36103  outsideofeq  36104  elicc3  36291  nn0prpwlem  36296  nndivsub  36431  fvineqsneu  37385  fvineqsneq  37386  ftc1anc  37681  cntotbnd  37776  heiborlem6  37796  pridlc3  38053  erimeq2  38656  leat2  39273  cvrexchlem  39398  cvratlem  39400  3dim2  39447  ps-2  39457  lncvrelatN  39760  osumcllem11N  39945  relpmin  44926  2reuimp0  47098  iccpartgt  47411  odz2prm2pw  47547  bgoldbachlt  47797  tgblthelfgott  47799  tgoldbach  47801  grimco  47873  isubgr3stgrlem6  47955  isubgr3stgrlem8  47957  uspgrlimlem2  47973  clnbgr3stgrgrlic  48004  gpgedgvtx0  48045  gpgedgvtx1  48046