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  652  3expb  1121  reuss2  4280  reupick  4283  po2nr  5554  tz7.7  6351  ordtr2  6370  fvmptt  6970  fliftfund  7269  isomin  7293  f1ocnv2d  7621  onint  7745  resf1extb  7886  soseq  8111  tz7.48lem  8382  oalimcl  8497  oaass  8498  omass  8517  omabs  8589  finsschain  9271  frmin  9673  infxpenlem  9935  axcc3  10360  zorn2lem7  10424  addclpi  10815  addnidpi  10824  genpnnp  10928  genpnmax  10930  mulclprlem  10942  dedekindle  11309  prodgt0  12000  ltsubrp  12955  ltaddrp  12956  pfxccat3  14669  sumeven  16326  sumodd  16327  lcmfunsnlem2lem1  16577  divgcdcoprm0  16604  infpnlem1  16850  prmgaplem4  16994  iscatd  17608  imasmnd2  18711  imasgrp2  18997  cyccom  19144  imasrng  20124  imasring  20278  funcrngcsetcALT  20586  mplcoe5lem  22006  dmatmul  22453  scmatmulcl  22474  scmatsgrp1  22478  smatvscl  22480  cpmatacl  22672  cpmatmcllem  22674  0ntr  23027  clsndisj  23031  innei  23081  islpi  23105  tgcnp  23209  haust1  23308  alexsublem  24000  alexsubb  24002  isxmetd  24282  bddiblnc  25811  2lgslem1a1  27368  nodense  27672  precsexlem11  28225  bdaypw2n0bndlem  28471  axcontlem4  29052  ewlkle  29691  clwwlkf  30134  clwwlknonwwlknonb  30193  uhgr3cyclexlem  30268  numclwwlk1lem2foa  30441  grpoidinvlem3  30594  elspansn5  31662  5oalem6  31747  mdi  32383  dmdi  32390  dmdsl3  32403  atom1d  32441  cvexchlem  32456  atcvatlem  32473  chirredlem3  32480  mdsymlem5  32495  f1o3d  32716  bnj570  35081  dfon2lem6  36002  broutsideof2  36338  outsideoftr  36345  outsideofeq  36346  elicc3  36533  nn0prpwlem  36538  nndivsub  36673  fvineqsneu  37666  fvineqsneq  37667  ftc1anc  37952  cntotbnd  38047  heiborlem6  38067  pridlc3  38324  erimeq2  39014  leat2  39670  cvrexchlem  39795  cvratlem  39797  3dim2  39844  ps-2  39854  lncvrelatN  40157  osumcllem11N  40342  relpmin  45308  2reuimp0  47474  iccpartgt  47787  odz2prm2pw  47923  bgoldbachlt  48173  tgblthelfgott  48175  tgoldbach  48177  grimco  48249  isubgr3stgrlem6  48331  isubgr3stgrlem8  48333  uspgrlimlem2  48349  clnbgr3stgrgrlic  48380  gpgedgvtx0  48421  gpgedgvtx1  48422