Theorem imp32 422

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imp42  430  impr  458  anasss  470  an13s  661  3expb  1133  reuss2  4278  reupick  4281  po2nr  5569  tz7.7  6372  ordtr2  6391  fvmptt  6996  fliftfund  7297  isomin  7321  f1ocnv2d  7649  onint  7773  resf1extb  7915  soseq  8139  tz7.48lem  8412  oalimcl  8529  oaass  8530  omass  8549  omabs  8621  finsschain  9302  frmin  9707  infxpenlem  9969  axcc3  10395  zorn2lem7  10459  addclpi  10850  addnidpi  10859  genpnnp  10963  genpnmax  10965  mulclprlem  10977  dedekindle  11347  prodgt0  12038  ltsubrp  13031  ltaddrp  13032  pfxccat3  14747  sumeven  16421  sumodd  16422  lcmfunsnlem2lem1  16672  divgcdcoprm0  16699  infpnlem1  16946  prmgaplem4  17090  iscatd  17705  imasmnd2  18808  imasgrp2  19097  cyccom  19244  imasrng  20223  imasring  20375  funcrngcsetcALT  20687  mplcoe5lem  22089  dmatmul  22554  scmatmulcl  22575  scmatsgrp1  22579  smatvscl  22581  cpmatacl  22773  cpmatmcllem  22775  0ntr  23128  clsndisj  23132  innei  23182  islpi  23206  tgcnp  23310  haust1  23409  alexsublem  24101  alexsubb  24103  isxmetd  24383  bddiblnc  25901  2lgslem1a1  27450  nodense  27753  precsexlem11  28307  bdaypw2n0bndlem  28553  axcontlem4  29165  ewlkle  29803  clwwlkf  30246  clwwlknonwwlknonb  30305  uhgr3cyclexlem  30380  numclwwlk1lem2foa  30553  grpoidinvlem3  30706  elspansn5  31774  5oalem6  31859  mdi  32495  dmdi  32502  dmdsl3  32515  atom1d  32553  cvexchlem  32568  atcvatlem  32585  chirredlem3  32592  mdsymlem5  32607  f1o3d  32825  bnj570  35197  dfon2lem6  36133  broutsideof2  36469  outsideoftr  36476  outsideofeq  36477  elicc3  36674  nn0prpwlem  36679  nndivsub  36814  fvineqsneu  37902  fvineqsneq  37903  ftc1anc  38197  cntotbnd  38292  heiborlem6  38312  pridlc3  38569  erimeq2  39259  leat2  39915  cvrexchlem  40040  cvratlem  40042  3dim2  40089  ps-2  40099  lncvrelatN  40402  osumcllem11N  40587  relpmin  45525  2reuimp0  47705  iccpartgt  48030  odz2prm2pw  48169  bgoldbachlt  48432  tgblthelfgott  48434  tgoldbach  48436  grimco  48508  isubgr3stgrlem6  48590  isubgr3stgrlem8  48592  uspgrlimlem2  48608  clnbgr3stgrgrlic  48639  gpgedgvtx0  48680  gpgedgvtx1  48681