Theorem 3expb 1134

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 1133	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 422	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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  df-3an 1101

This theorem is referenced by:  3expia  1135  3adant3r1  1197  3adant3r2  1198  3adant3r3  1199  mp3an1  1470  sotri  6115  fnfco  6730  mpoeq3dva  7474  oprres  7565  fovcdmda  7568  fnmpoovd  8067  offval22  8068  bropfvvvvlem  8071  fnsuppres  8172  suppsssn  8182  sprmpod  8205  oaass  8531  omlimcl  8548  odi  8549  nnmsucr  8596  nnasmo  8634  unfi  9140  ttrclse  9683  cflim2  10221  mulcanenq  10919  mul4  11352  add4  11405  2addsub  11445  addsubeq4  11446  subadd4  11476  muladd  11620  ltleadd  11671  divmul  11849  divne0  11858  div23  11865  div12  11868  div11  11874  divsubdir  11885  subdivcomb1  11887  divcan5  11894  divmuleq  11897  divcan6  11899  divdiv32  11900  div2sub  12017  letrp1  12036  lemul12b  12049  lediv1  12058  lt2mul2div  12071  lemuldiv  12073  ltdiv2  12079  ledivdiv  12082  lediv2  12083  ltdiv23  12084  lediv23  12085  sup2  12149  cju  12192  nndivre  12255  nndivtr  12261  nn0addge1  12528  nn0addge2  12529  peano2uz2  12662  uzind  12666  uzind3  12668  fzind  12672  fnn0ind  12673  uzind4  12908  qre  12955  irrmul  12976  rpdivcl  13021  rerpdivcl  13026  xrinfmsslem  13312  ixxin  13367  iccshftr  13491  iccshftl  13493  iccdil  13495  icccntr  13497  fzaddel  13564  fzadd2  13565  fzrev  13593  modlt  13891  modcyc  13917  axdc4uzlem  13997  expdiv  14127  fundmge2nop0  14516  swrd00  14659  swrdcl  14660  swrdnnn0nd  14671  swrd0  14673  swrdwrdsymb  14677  ccatpfx  14715  swrdccat  14749  splid  14767  swrdco  14851  2shfti  15094  isermulc2  15686  fsummulc2  15812  dvdscmulr  16319  dvdsmulcr  16320  dvds2add  16325  dvds2sub  16326  dvdstr  16329  alzdvds  16355  divalg2  16440  dvdslegcd  16539  lcmgcdlem  16641  lcmgcdeq  16647  isprm6  16750  pcqcl  16893  vdwmc2  17016  ressinbas  17282  cicer  17840  isposd  18355  pleval2i  18367  poslubmo  18442  posglbmo  18443  tosso  18450  mgmplusf  18685  ismgmd  18687  grpinva  18709  idmgmhm  18736  resmgmhm  18746  resmgmhm2  18747  resmgmhm2b  18748  mgmhmco  18749  mgmhmima  18750  submgmacs  18752  sgrpidmnd  18774  ismndd  18791  imasmnd2  18809  idmhm  18830  mndvcl  18832  issubm2  18839  0mhm  18854  resmhm  18855  resmhm2  18856  resmhm2b  18857  mhmco  18858  mhmimalem  18859  submacs  18862  prdspjmhm  18864  pwsdiagmhm  18866  pwsco1mhm  18867  pwsco2mhm  18868  gsumwsubmcl  18872  gsumsgrpccat  18875  gsumwmhm  18880  grpinvcnv  19049  grpinvnzcl  19054  grpsubf  19062  imasgrp2  19098  qusgrp2  19101  mhmfmhm  19108  mulgnnsubcl  19129  mulgnndir  19146  issubg4  19188  isnsg3  19202  nsgacs  19204  nsgid  19212  qusadd  19230  qus0subgadd  19241  ghmmhm  19267  ghmmhmb  19268  idghm  19272  resghm  19273  ghmf1  19287  qusghm  19296  gaid  19340  subgga  19341  gasubg  19343  invoppggim  19401  gsmsymgrfix  19469  smndlsmidm  19697  pj1ghm  19744  mulgnn0di  19866  mulgmhm  19868  mulgghm  19869  ghmfghm  19871  invghm  19874  ghmplusg  19887  ablnsg  19888  qusabl  19906  gsumval3eu  19945  gsumval3  19948  gsumzcl2  19951  gsumzaddlem  19962  gsumzadd  19963  gsumzmhm  19978  gsumzoppg  19985  srgfcl  20247  srgcom4lem  20264  srgmulgass  20268  srglmhm  20272  srgrmhm  20273  ringcomlem  20330  ringlghm  20363  ringrghm  20364  pwspjmhmmgpd  20377  c0mgm  20509  c0mhm  20510  isnzr2  20569  subrngringnsg  20604  issubrng2  20609  rhmimasubrnglem  20616  issubrg2  20643  domnmuln0  20760  isdomn3  20766  issrngd  20905  islmodd  20934  lmodscaf  20952  lcomf  20969  lmodvsghm  20991  rmodislmodlem  20997  lssacs  21035  idlmhm  21109  invlmhm  21110  lmhmvsca  21113  reslmhm2  21121  reslmhm2b  21122  pwsdiaglmhm  21125  pwssplit2  21128  pwssplit3  21129  issubrgd  21257  qusrhm  21347  qusmul2idl  21350  crngridl  21351  qusmulrng  21353  expmhm  21489  zntoslem  21609  znfld  21613  psgnghm  21633  phlipf  21705  frlmup1  21851  asclghm  21935  asclrhm  21943  rnasclmulcl  21947  psraddcl  21992  psrvscacl  22004  psrass23  22021  psrbagev1  22131  coe1sclmulfv  22347  cply1mul  22360  evls1fpws  22433  rhmply1vsca  22449  matbas2d  22484  submaeval  22643  minmar1eval  22710  cpmatacl  22777  pmatcollpw1  22837  pmatcollpw  22842  tgclb  23031  topbas  23033  ntrss  23116  mretopd  23153  neissex  23188  cnpnei  23325  lmcnp  23365  ordthaus  23445  llynlly  23538  restnlly  23543  llyidm  23549  nllyidm  23550  ptbasin  23638  txcnp  23681  ist0-4  23790  kqt0lem  23797  isr0  23798  regr1lem2  23801  cmphmph  23849  connhmph  23850  fbun  23901  trfbas2  23904  isfil2  23917  isfild  23919  infil  23924  fbasfip  23929  fbasrn  23945  trfil2  23948  rnelfmlem  24013  fmfnfmlem3  24017  flimopn  24036  txflf  24067  fclsnei  24080  fclsfnflim  24088  fcfnei  24096  clssubg  24170  tgphaus  24178  qustgplem  24182  tsmsadd  24208  psmetxrge0  24374  psmetlecl  24376  xmetlecl  24407  xmettpos  24410  imasdsf1olem  24434  imasf1oxmet  24436  imasf1omet  24437  elbl3ps  24452  elbl3  24453  metss  24569  comet  24574  stdbdxmet  24576  stdbdmet  24577  methaus  24581  nrmmetd  24635  abvmet  24636  isngp4  24673  subgngp  24696  nmoi2  24791  nmoleub  24792  nmoid  24803  bl2ioo  24853  zcld  24875  divcn  24931  divccn  24936  cncfcdm  24961  divccncf  24969  icoopnst  25002  clmzlmvsca  25176  cph2ass  25276  tcphcph  25300  cfilfcls  25337  bcthlem2  25388  rrxmet  25471  rrxdstprj1  25472  rrxdsfi  25474  cldcss  25504  dvrec  26018  dvmptfsum  26038  aalioulem3  26399  taylply2  26432  efsubm  26617  dchrelbasd  27304  dchrmulcl  27314  2sqreulem3  27518  pntrmax  27629  padicabv  27695  nosupbnd2  27781  noinfbnd2  27796  sltsd  27862  divmulsw  28287  axtgcont  28639  xmstrkgc  29087  axsegconlem1  29119  axlowdimlem15  29158  usgredg2vlem1  29427  usgredg2vlem2  29428  iswlkon  29857  wwlksnextsurj  30101  elwwlks2  30170  elwspths2spth  30171  frrusgrord  30544  numclwwlk1lem2foalem  30554  grpoidinvlem2  30709  grpoidinvlem3  30710  ablo4  30754  ablomuldiv  30756  nvaddsub4  30861  nvmeq0  30862  sspmval  30937  sspimsval  30942  lnosub  30963  dipsubdir  31052  hvadd4  31240  hvpncan  31243  his35  31292  hiassdi  31295  shscli  31521  shmodsi  31593  chj4  31739  spansnmul  31768  spansncol  31772  spanunsni  31783  hoadd4  31988  hosubadd4  32018  lnopl  32118  unopf1o  32120  counop  32125  lnfnl  32135  hmopadj2  32145  eighmre  32167  lnopmi  32204  lnophsi  32205  hmops  32224  hmopm  32225  cnlnadjlem2  32272  adjmul  32296  adjadd  32297  kbass6  32325  mdslj1i  32523  mdslj2i  32524  mdslmd1lem1  32529  mdslmd2i  32534  chirredlem3  32596  isoun  32905  xdivmul  33103  odutos  33147  lmodvslmhm  33231  isarchi2  33366  archiabllem2  33378  imasmhm  33541  imasghm  33542  imasrhm  33543  imaslmhm  33544  quslmhm  33546  tngdim  33911  fedgmullem2  33928  metider  34192  pl1cn  34253  rossros  34478  ismeas  34497  dya2iocnei  34580  inelcarsg  34609  signstfvc  34869  bnj563  35040  fisshasheq  35466  cnpconn  35581  cvmseu  35627  elmrsubrn  35871  mrsubco  35872  fneint  36709  fnessref  36718  tailfb  36738  onsucuni3  37862  pibt2  37912  ptrecube  38120  poimirlem4  38124  heicant  38155  mblfinlem1  38157  mblfinlem2  38158  mblfinlem3  38159  mblfinlem4  38160  cnambfre  38168  itg2addnclem2  38172  ftc1anclem5  38197  ftc1anclem6  38198  metf1o  38255  isbnd3b  38285  equivbnd  38290  heiborlem3  38313  rrnmet  38329  rrndstprj1  38330  rrntotbnd  38336  exidcl  38376  ghomco  38391  ghomdiv  38392  grpokerinj  38393  rngoneglmul  38443  rngonegrmul  38444  rngosubdi  38445  rngosubdir  38446  isdrngo2  38458  rngohomco  38474  rngoisocnv  38481  riscer  38488  crngm4  38503  crngohomfo  38506  idlsubcl  38523  inidl  38530  keridl  38532  ispridlc  38570  pridlc3  38573  dmncan1  38576  lflvscl  39702  3dim0  40082  linepsubN  40377  cdlemg2fvlem  41219  trlcoat  41348  istendod  41387  dva1dim  41610  dvhvaddcomN  41721  dihf11  41892  dihlatat  41962  sn-sup2  43114  fsuppssind  43176  mhphf  43180  ismrc  43283  isnacs3  43292  mzpindd  43328  pellex  43413  monotoddzzfi  43520  lermxnn0  43528  rmyeq0  43531  rmyeq  43532  lermy  43533  jm2.27  43586  lsmfgcl  43652  fsumcnsrcl  43744  rngunsnply  43747  gsumws3  44773  mnringmulrcld  44805  nzin  44895  ofdivrec  44903  ofdivcan4  44904  chordthmALT  45509  wessf1ornlem  45764  projf1o  45775  ltdiv23neg  45970  fmulcl  46158  prproropf1olem2  48111  prproropf1olem4  48113  mgmplusgiopALT  48817  itsclc0xyqsolb  49393  toslat  49604  cicerALT  49668