Theorem 3expb 1121

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expb	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 420	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3expia  1122  3adant3r1  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1449  sotri  6126  fnfco  6754  mpoeq3dva  7483  oprres  7572  fovcdmda  7575  fnmpoovd  8070  offval22  8071  bropfvvvvlem  8074  fnsuppres  8173  suppsssn  8183  sprmpod  8206  oaass  8558  omlimcl  8575  odi  8576  nnmsucr  8622  nnasmo  8659  unfi  9169  ttrclse  9719  cflim2  10255  mulcanenq  10952  mul4  11379  add4  11431  2addsub  11471  addsubeq4  11472  subadd4  11501  muladd  11643  ltleadd  11694  divmul  11872  divne0  11881  div23  11888  div12  11891  divsubdir  11905  subdivcomb1  11906  divcan5  11913  divmuleq  11916  divcan6  11918  divdiv32  11919  div2sub  12036  letrp1  12055  lemul12b  12068  lediv1  12076  lt2mul2div  12089  lemuldiv  12091  ltdiv2  12097  ledivdiv  12100  lediv2  12101  ltdiv23  12102  lediv23  12103  sup2  12167  cju  12205  nndivre  12250  nndivtr  12256  nn0addge1  12515  nn0addge2  12516  peano2uz2  12647  uzind  12651  uzind3  12653  fzind  12657  fnn0ind  12658  uzind4  12887  qre  12934  irrmul  12955  rpdivcl  12996  rerpdivcl  13001  xrinfmsslem  13284  ixxin  13338  iccshftr  13460  iccshftl  13462  iccdil  13464  icccntr  13466  fzaddel  13532  fzadd2  13533  fzrev  13561  modlt  13842  modcyc  13868  axdc4uzlem  13945  expdiv  14076  fundmge2nop0  14450  swrd00  14591  swrdcl  14592  swrdnnn0nd  14603  swrd0  14605  swrdwrdsymb  14609  ccatpfx  14648  swrdccat  14682  splid  14700  swrdco  14785  2shfti  15024  isermulc2  15601  fsummulc2  15727  dvdscmulr  16225  dvdsmulcr  16226  dvds2add  16230  dvds2sub  16231  dvdstr  16234  alzdvds  16260  divalg2  16345  dvdslegcd  16442  lcmgcdlem  16540  lcmgcdeq  16546  isprm6  16648  pcqcl  16786  vdwmc2  16909  ressinbas  17187  cicer  17750  isposd  18273  pleval2i  18286  poslubmo  18361  posglbmo  18362  tosso  18369  mgmplusf  18568  grpinva  18590  sgrpidmnd  18627  ismndd  18644  imasmnd2  18659  idmhm  18678  issubm2  18682  0mhm  18697  resmhm  18698  resmhm2  18699  resmhm2b  18700  mhmco  18701  mhmimalem  18702  submacs  18705  prdspjmhm  18707  pwsdiagmhm  18709  pwsco1mhm  18710  pwsco2mhm  18711  gsumwsubmcl  18715  gsumsgrpccat  18718  gsumwmhm  18723  grpinvcnv  18888  grpinvnzcl  18892  grpsubf  18899  imasgrp2  18935  qusgrp2  18938  mhmfmhm  18943  mulgnnsubcl  18961  mulgnndir  18978  issubg4  19020  isnsg3  19035  nsgacs  19037  nsgid  19045  qusadd  19062  qus0subgadd  19071  ghmmhm  19097  ghmmhmb  19098  idghm  19102  resghm  19103  ghmf1  19116  qusghm  19124  gaid  19158  subgga  19159  gasubg  19161  invoppggim  19222  gsmsymgrfix  19291  smndlsmidm  19519  pj1ghm  19566  mulgnn0di  19688  mulgmhm  19690  mulgghm  19691  ghmfghm  19693  invghm  19696  ghmplusg  19709  ablnsg  19710  qusabl  19728  gsumval3eu  19767  gsumval3  19770  gsumzcl2  19773  gsumzaddlem  19784  gsumzadd  19785  gsumzmhm  19800  gsumzoppg  19807  srgfcl  20013  srgcom4lem  20030  srgmulgass  20034  srglmhm  20038  srgrmhm  20039  ringcomlem  20090  ringlghm  20118  ringrghm  20119  pwspjmhmmgpd  20135  isnzr2  20290  issubrg2  20376  issrngd  20462  islmodd  20470  lmodscaf  20487  lcomf  20504  lmodvsghm  20526  rmodislmodlem  20532  lssacs  20571  idlmhm  20645  invlmhm  20646  lmhmvsca  20649  reslmhm2  20657  reslmhm2b  20658  pwsdiaglmhm  20661  pwssplit2  20664  pwssplit3  20665  issubrgd  20804  qusrhm  20867  qusmul2  20868  crngridl  20869  quscrng  20871  domnmuln0  20907  opprdomn  20912  expmhm  21007  zntoslem  21104  znfld  21108  psgnghm  21125  phlipf  21197  frlmup1  21345  asclghm  21429  asclrhm  21436  rnasclmulcl  21440  psraddcl  21494  psrvscacl  21504  psrass23  21522  psrbagev1  21630  psrbagev1OLD  21631  coe1sclmulfv  21797  cply1mul  21810  mndvcl  21885  matbas2d  21917  submaeval  22076  minmar1eval  22143  cpmatacl  22210  pmatcollpw1  22270  pmatcollpw  22275  tgclb  22465  topbas  22467  ntrss  22551  mretopd  22588  neissex  22623  cnpnei  22760  lmcnp  22800  ordthaus  22880  llynlly  22973  restnlly  22978  llyidm  22984  nllyidm  22985  ptbasin  23073  txcnp  23116  ist0-4  23225  kqt0lem  23232  isr0  23233  regr1lem2  23236  cmphmph  23284  connhmph  23285  fbun  23336  trfbas2  23339  isfil2  23352  isfild  23354  infil  23359  fbasfip  23364  fbasrn  23380  trfil2  23383  rnelfmlem  23448  fmfnfmlem3  23452  flimopn  23471  txflf  23502  fclsnei  23515  fclsfnflim  23523  fcfnei  23531  clssubg  23605  tgphaus  23613  qustgplem  23617  tsmsadd  23643  psmetxrge0  23811  psmetlecl  23813  xmetlecl  23844  xmettpos  23847  imasdsf1olem  23871  imasf1oxmet  23873  imasf1omet  23874  elbl3ps  23889  elbl3  23890  metss  24009  comet  24014  stdbdxmet  24016  stdbdmet  24017  methaus  24021  nrmmetd  24075  abvmet  24076  isngp4  24113  subgngp  24136  nmoi2  24239  nmoleub  24240  nmoid  24251  bl2ioo  24300  zcld  24321  divcn  24376  divccn  24381  cncfcdm  24406  divccncf  24414  icoopnst  24447  clmzlmvsca  24621  cph2ass  24722  tcphcph  24746  cfilfcls  24783  bcthlem2  24834  rrxmet  24917  rrxdstprj1  24918  rrxdsfi  24920  cldcss  24950  dvrec  25464  dvmptfsum  25484  aalioulem3  25839  taylply2  25872  efsubm  26052  dchrelbasd  26732  dchrmulcl  26742  2sqreulem3  26946  pntrmax  27057  padicabv  27123  nosupbnd2  27209  noinfbnd2  27224  ssltd  27283  divsmulw  27630  axtgcont  27710  xmstrkgc  28133  axsegconlem1  28165  axlowdimlem15  28204  usgredg2vlem1  28472  usgredg2vlem2  28473  iswlkon  28904  wwlksnextsurj  29144  elwwlks2  29210  elwspths2spth  29211  frrusgrord  29584  numclwwlk1lem2foalem  29594  grpoidinvlem2  29746  grpoidinvlem3  29747  ablo4  29791  ablomuldiv  29793  nvaddsub4  29898  nvmeq0  29899  sspmval  29974  sspimsval  29979  lnosub  30000  dipsubdir  30089  hvadd4  30277  hvpncan  30280  his35  30329  hiassdi  30332  shscli  30558  shmodsi  30630  chj4  30776  spansnmul  30805  spansncol  30809  spanunsni  30820  hoadd4  31025  hosubadd4  31055  lnopl  31155  unopf1o  31157  counop  31162  lnfnl  31172  hmopadj2  31182  eighmre  31204  lnopmi  31241  lnophsi  31242  hmops  31261  hmopm  31262  cnlnadjlem2  31309  adjmul  31333  adjadd  31334  kbass6  31362  mdslj1i  31560  mdslj2i  31561  mdslmd1lem1  31566  mdslmd2i  31571  chirredlem3  31633  isoun  31911  xdivmul  32079  odutos  32126  lmodvslmhm  32190  isarchi2  32319  archiabllem2  32331  quslmhm  32459  qusmul  32504  evls1fpws  32635  tngdim  32687  fedgmullem2  32704  metider  32863  pl1cn  32924  rossros  33167  ismeas  33186  dya2iocnei  33270  inelcarsg  33299  signstfvc  33574  bnj563  33743  fisshasheq  34093  cnpconn  34210  cvmseu  34256  elmrsubrn  34500  mrsubco  34501  gg-divcn  35152  gg-divccn  35154  fneint  35222  fnessref  35231  tailfb  35251  onsucuni3  36237  pibt2  36287  ptrecube  36477  poimirlem4  36481  heicant  36512  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  cnambfre  36525  itg2addnclem2  36529  ftc1anclem5  36554  ftc1anclem6  36555  metf1o  36612  isbnd3b  36642  equivbnd  36647  heiborlem3  36670  rrnmet  36686  rrndstprj1  36687  rrntotbnd  36693  exidcl  36733  ghomco  36748  ghomdiv  36749  grpokerinj  36750  rngoneglmul  36800  rngonegrmul  36801  rngosubdi  36802  rngosubdir  36803  isdrngo2  36815  rngohomco  36831  rngoisocnv  36838  riscer  36845  crngm4  36860  crngohomfo  36863  idlsubcl  36880  inidl  36887  keridl  36889  ispridlc  36927  pridlc3  36930  dmncan1  36933  lflvscl  37936  3dim0  38317  linepsubN  38612  cdlemg2fvlem  39454  trlcoat  39583  istendod  39622  dva1dim  39845  dvhvaddcomN  39956  dihf11  40127  dihlatat  40197  metakunt12  40985  fsuppssind  41163  mhphf  41167  sn-sup2  41339  ismrc  41425  isnacs3  41434  mzpindd  41470  pellex  41559  monotoddzzfi  41667  lermxnn0  41675  rmyeq0  41678  rmyeq  41679  lermy  41680  jm2.27  41733  lsmfgcl  41802  fsumcnsrcl  41894  rngunsnply  41901  isdomn3  41932  gsumws3  42934  mnringmulrcld  42973  nzin  43063  ofdivrec  43071  ofdivcan4  43072  chordthmALT  43680  wessf1ornlem  43868  projf1o  43882  ltdiv23neg  44091  fmulcl  44284  prproropf1olem2  46159  prproropf1olem4  46161  ismgmd  46533  idmgmhm  46545  resmgmhm  46555  resmgmhm2  46556  resmgmhm2b  46557  mgmhmco  46558  mgmhmima  46559  submgmacs  46561  mgmplusgiopALT  46591  c0mgm  46694  c0mhm  46695  subrngringnsg  46717  issubrng2  46722  rhmimasubrnglem  46729  qusmulrng  46752  itsclc0xyqsolb  47410  toslat  47561