Theorem imp32 448

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp32	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		impd.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 446	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 444	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  imp42  618  impr  647  anasss  677  an13s  841  3expb  1258  reuss2  3866  reupick  3870  po2nr  4972  tz7.7  5666  ordtr2  5685  fvmptt  6208  fliftfund  6463  isomin  6487  f1ocnv2d  6784  onint  6887  tz7.48lem  7423  oalimcl  7527  oaass  7528  omass  7547  omabs  7614  finsschain  8156  infxpenlem  8719  axcc3  9143  zorn2lem7  9207  addclpi  9593  addnidpi  9602  genpnnp  9706  genpnmax  9708  mulclprlem  9720  dedekindle  10080  prodgt0  10747  ltsubrp  11742  ltaddrp  11743  swrdccatin1  13334  swrdccat3  13343  sumeven  14948  sumodd  14949  lcmfunsnlem2lem1  15189  divgcdcoprm0  15217  infpnlem1  15452  prmgaplem4  15596  iscatd  16157  imasmnd2  17150  imasgrp2  17353  imasring  18442  mplcoe5lem  19288  dmatmul  20122  scmatmulcl  20143  scmatsgrp1  20147  smatvscl  20149  cpmatacl  20340  cpmatmcllem  20342  0ntr  20685  clsndisj  20689  innei  20739  islpi  20763  tgcnp  20867  haust1  20966  alexsublem  21658  alexsubb  21660  isxmetd  21941  2lgslem1a1  24914  axcontlem4  25647  wwlknimp  26215  wlkiswwlksur  26247  clwwlkf  26322  clwwlkextfrlem1  26603  grpoidinvlem3  26744  elspansn5  27817  5oalem6  27902  mdi  28538  dmdi  28545  dmdsl3  28558  atom1d  28596  cvexchlem  28611  atcvatlem  28628  chirredlem3  28635  mdsymlem5  28650  f1o3d  28813  bnj570  30229  dfon2lem6  30937  frmin  30983  soseq  30995  nodenselem5  31084  nodense  31088  broutsideof2  31399  outsideoftr  31406  outsideofeq  31407  elicc3  31481  nn0prpwlem  31487  nndivsub  31626  bddiblnc  32650  ftc1anc  32663  cntotbnd  32765  heiborlem6  32785  pridlc3  33042  leat2  33599  cvrexchlem  33723  cvratlem  33725  3dim2  33772  ps-2  33782  lncvrelatN  34085  osumcllem11N  34270  iccpartgt  39965  odz2prm2pw  40013  bgoldbachlt  40227  tgblthelfgott  40229  tgoldbach  40232  bgoldbachltOLD  40234  tgblthelfgottOLD  40236  tgoldbachOLD  40239  pfxccat3  40289  ewlkle  40807  wlkwwlksur  41094  clwwlksf  41222  uhgr3cyclexlem  41348  av-clwwlkextfrlem1  41509  funcrngcsetcALT  41791