Theorem imp32 423

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp42  431  impr  459  anasss  471  an13s  663  3expb  1138  reuss2  4279  reupick  4282  po2nr  5583  tz7.7  6386  ordtr2  6406  fvmptt  7010  fliftfund  7311  isomin  7335  f1ocnv2d  7663  onint  7785  resf1extb  7927  soseq  8151  tz7.48lem  8424  oalimcl  8541  oaass  8542  omass  8561  omabs  8633  finsschain  9312  frmin  9717  infxpenlem  9993  axcc3  10417  zorn2lem7  10481  addclpi  10872  addnidpi  10881  genpnnp  10985  genpnmax  10987  mulclprlem  10999  dedekindle  11369  prodgt0  12057  ltsubrp  13049  ltaddrp  13050  pfxccat3  14767  sumeven  16440  sumodd  16441  lcmfunsnlem2lem1  16691  divgcdcoprm0  16718  infpnlem1  16965  prmgaplem4  17109  iscatd  17724  imasmnd2  18827  imasgrp2  19116  cyccom  19269  imasrng  20250  imasring  20408  funcrngcsetcALT  20740  cmprmidlmcl  21475  mplcoe5lem  22190  dmatmul  22654  scmatmulcl  22675  scmatsgrp1  22679  smatvscl  22681  cpmatacl  22873  cpmatmcllem  22875  0ntr  23228  clsndisj  23232  innei  23282  islpi  23306  tgcnp  23410  haust1  23509  alexsublem  24201  alexsubb  24203  isxmetd  24483  bddiblnc  26001  2lgslem1a1  27553  nodense  27856  precsexlem11  28410  bdaypw2n0bndlem  28656  axcontlem4  29317  ewlkle  29955  clwwlkf  30398  clwwlknonwwlknonb  30457  uhgr3cyclexlem  30532  numclwwlk1lem2foa  30705  grpoidinvlem3  30858  elspansn5  31926  5oalem6  32011  mdi  32647  dmdi  32654  dmdsl3  32667  atom1d  32705  cvexchlem  32720  atcvatlem  32737  chirredlem3  32744  mdsymlem5  32759  f1o3d  32971  bnj570  35293  dfon2lem6  36278  broutsideof2  36614  outsideoftr  36621  outsideofeq  36622  elicc3  36828  nn0prpwlem  36833  nndivsub  36968  fvineqsneu  38057  fvineqsneq  38058  ftc1anc  38352  cntotbnd  38447  heiborlem6  38467  pridlc3  38724  erimeq2  39412  leat2  40068  cvrexchlem  40193  cvratlem  40195  3dim2  40242  ps-2  40252  lncvrelatN  40555  osumcllem11N  40740  relpmin  45661  2reuimp0  47851  iccpartgt  48176  odz2prm2pw  48315  bgoldbachlt  48578  tgblthelfgott  48580  tgoldbach  48582  grimco  48654  isubgr3stgrlem6  48736  isubgr3stgrlem8  48738  uspgrlimlem2  48754  clnbgr3stgrgrlic  48785  gpgedgvtx0  48826  gpgedgvtx1  48827