Theorem 3expb 1136

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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

This theorem is referenced by:  3expia  1137  3adant3r1  1199  3adant3r2  1200  3adant3r3  1201  mp3an1  1474  sotri  6128  fnfco  6744  mpoeq3dva  7488  oprres  7579  fovcdmda  7582  fnmpoovd  8082  offval22  8083  bropfvvvvlem  8086  fnsuppres  8187  suppsssn  8197  sprmpod  8220  oaass  8546  omlimcl  8563  odi  8564  nnmsucr  8611  nnasmo  8649  unfi  9155  ttrclse  9696  cflim2  10247  mulcanenq  10945  mul4  11378  add4  11431  2addsub  11471  addsubeq4  11472  subadd4  11502  muladd  11646  ltleadd  11697  divmul  11875  divne0  11884  div23  11891  div12  11894  div11  11900  divsubdir  11908  subdivcomb1  11910  divcan5  11917  divmuleq  11920  divcan6  11922  divdiv32  11923  div2sub  12040  letrp1  12059  lemul12b  12072  lediv1  12080  lt2mul2div  12093  lemuldiv  12095  ltdiv2  12101  ledivdiv  12104  lediv2  12105  ltdiv23  12106  lediv23  12107  sup2  12171  cju  12214  nndivre  12277  nndivtr  12283  nn0addge1  12550  nn0addge2  12551  peano2uz2  12684  uzind  12688  uzind3  12690  fzind  12694  fnn0ind  12695  uzind4  12930  qre  12977  irrmul  12998  rpdivcl  13043  rerpdivcl  13048  xrinfmsslem  13334  ixxin  13389  iccshftr  13513  iccshftl  13515  iccdil  13517  icccntr  13519  fzaddel  13586  fzadd2  13587  fzrev  13615  modlt  13913  modcyc  13939  axdc4uzlem  14019  expdiv  14149  fundmge2nop0  14539  swrd00  14682  swrdcl  14683  swrdnnn0nd  14694  swrd0  14696  swrdwrdsymb  14700  ccatpfx  14738  swrdccat  14772  splid  14790  swrdco  14874  2shfti  15117  isermulc2  15709  fsummulc2  15835  dvdscmulr  16342  dvdsmulcr  16343  dvds2add  16348  dvds2sub  16349  dvdstr  16352  alzdvds  16378  divalg2  16463  dvdslegcd  16562  lcmgcdlem  16664  lcmgcdeq  16670  isprm6  16773  pcqcl  16916  vdwmc2  17039  ressinbas  17305  cicer  17863  isposd  18378  pleval2i  18390  poslubmo  18465  posglbmo  18466  tosso  18473  mgmplusf  18708  ismgmd  18710  grpinva  18732  idmgmhm  18759  resmgmhm  18769  resmgmhm2  18770  resmgmhm2b  18771  mgmhmco  18772  mgmhmima  18773  submgmacs  18775  sgrpidmnd  18797  ismndd  18814  imasmnd2  18832  idmhm  18853  mndvcl  18855  issubm2  18862  0mhm  18878  resmhm  18879  resmhm2  18880  resmhm2b  18881  mhmco  18882  mhmimalem  18883  submacs  18886  prdspjmhm  18888  pwsdiagmhm  18890  pwsco1mhm  18891  pwsco2mhm  18892  gsumwsubmcl  18896  gsumsgrpccat  18899  gsumwmhm  18904  grpinvcnv  19073  grpinvnzcl  19077  grpsubf  19085  imasgrp2  19121  qusgrp2  19124  mhmfmhm  19131  mulgnnsubcl  19152  mulgnndir  19169  issubg4  19212  isnsg3  19226  nsgacs  19228  nsgid  19236  qusadd  19259  qus0subgadd  19270  ghmmhm  19296  ghmmhmb  19297  idghm  19301  resghm  19302  ghmf1  19316  qusghm  19325  gaid  19369  subgga  19370  gasubg  19372  invoppggim  19430  gsmsymgrfix  19498  smndlsmidm  19726  pj1ghm  19773  mulgnn0di  19895  mulgmhm  19897  mulgghm  19898  ghmfghm  19900  invghm  19903  ghmplusg  19916  ablnsg  19917  qusabl  19935  gsumval3eu  19974  gsumval3  19977  gsumzcl2  19980  gsumzaddlem  19991  gsumzadd  19992  gsumzmhm  20007  gsumzoppg  20014  srgfcl  20278  srgcom4lem  20295  srgmulgass  20299  srglmhm  20303  srgrmhm  20304  ringcomlem  20362  ringlghm  20395  ringrghm  20396  pwspjmhmmgpd  20409  c0mgm  20541  c0mhm  20542  isnzr2  20601  subrngringnsg  20638  issubrng2  20643  rhmimasubrnglem  20650  issubrg2  20677  domnmuln0  20794  isdomn3  20799  issrngd  20936  islmodd  20965  lmodscaf  20983  lcomf  21000  lmodvsghm  21022  rmodislmodlem  21028  lssacs  21066  idlmhm  21140  invlmhm  21141  lmhmvsca  21144  reslmhm2  21152  reslmhm2b  21153  pwsdiaglmhm  21156  pwssplit2  21159  pwssplit3  21160  issubrgd  21288  qusrhm  21386  qusmul2idl  21389  crngridl  21390  qusmulrng  21393  expmhm  21555  zntoslem  21675  znfld  21679  psgnghm  21699  phlipf  21771  frlmup1  21917  asclghm  22001  asclrhm  22009  rnasclmulcl  22013  psraddcl  22058  psrvscacl  22070  psrass23  22087  psrbagev1  22197  coe1sclmulfv  22413  cply1mul  22425  evls1fpws  22498  rhmply1vsca  22514  matbas2d  22549  submaeval  22708  minmar1eval  22775  cpmatacl  22842  pmatcollpw1  22902  pmatcollpw  22907  tgclb  23096  topbas  23098  ntrss  23181  mretopd  23218  neissex  23253  cnpnei  23390  lmcnp  23430  ordthaus  23510  llynlly  23603  restnlly  23608  llyidm  23614  nllyidm  23615  ptbasin  23703  txcnp  23746  ist0-4  23855  kqt0lem  23862  isr0  23863  regr1lem2  23866  cmphmph  23914  connhmph  23915  fbun  23966  trfbas2  23969  isfil2  23982  isfild  23984  infil  23989  fbasfip  23994  fbasrn  24010  trfil2  24013  rnelfmlem  24078  fmfnfmlem3  24082  flimopn  24101  txflf  24132  fclsnei  24145  fclsfnflim  24153  fcfnei  24161  clssubg  24235  tgphaus  24243  qustgplem  24247  tsmsadd  24273  psmetxrge0  24439  psmetlecl  24441  xmetlecl  24472  xmettpos  24475  imasdsf1olem  24499  imasf1oxmet  24501  imasf1omet  24502  elbl3ps  24517  elbl3  24518  metss  24634  comet  24639  stdbdxmet  24641  stdbdmet  24642  methaus  24646  nrmmetd  24700  abvmet  24701  isngp4  24738  subgngp  24761  nmoi2  24856  nmoleub  24857  nmoid  24868  bl2ioo  24918  zcld  24940  divcn  24996  divccn  25001  cncfcdm  25026  divccncf  25034  icoopnst  25067  clmzlmvsca  25241  cph2ass  25341  tcphcph  25365  cfilfcls  25402  bcthlem2  25453  rrxmet  25536  rrxdstprj1  25537  rrxdsfi  25539  cldcss  25569  dvrec  26083  dvmptfsum  26103  aalioulem3  26464  taylply2  26497  efsubm  26682  dchrelbasd  27369  dchrmulcl  27379  2sqreulem3  27583  pntrmax  27694  padicabv  27760  nosupbnd2  27846  noinfbnd2  27861  sltsd  27927  divmulsw  28352  axtgcont  28704  xmstrkgc  29176  axsegconlem1  29208  axlowdimlem15  29247  usgredg2vlem1  29516  usgredg2vlem2  29517  iswlkon  29946  wwlksnextsurj  30190  elwwlks2  30259  elwspths2spth  30260  frrusgrord  30633  numclwwlk1lem2foalem  30643  grpoidinvlem2  30798  grpoidinvlem3  30799  ablo4  30843  ablomuldiv  30845  nvaddsub4  30950  nvmeq0  30951  sspmval  31026  sspimsval  31031  lnosub  31052  dipsubdir  31141  hvadd4  31329  hvpncan  31332  his35  31381  hiassdi  31384  shscli  31610  shmodsi  31682  chj4  31828  spansnmul  31857  spansncol  31861  spanunsni  31872  hoadd4  32077  hosubadd4  32107  lnopl  32207  unopf1o  32209  counop  32214  lnfnl  32224  hmopadj2  32234  eighmre  32256  lnopmi  32293  lnophsi  32294  hmops  32313  hmopm  32314  cnlnadjlem2  32361  adjmul  32385  adjadd  32386  kbass6  32414  mdslj1i  32612  mdslj2i  32613  mdslmd1lem1  32618  mdslmd2i  32623  chirredlem3  32685  isoun  32988  xdivmul  33185  odutos  33229  lmodvslmhm  33311  isarchi2  33446  archiabllem2  33458  imasmhm  33617  imasghm  33618  imasrhm  33619  imaslmhm  33620  quslmhm  33622  tngdim  33948  fedgmullem2  33965  metider  34229  pl1cn  34290  rossros  34515  ismeas  34534  dya2iocnei  34617  inelcarsg  34646  signstfvc  34906  bnj563  35077  fisshasheq  35539  cnpconn  35655  cvmseu  35701  elmrsubrn  35945  mrsubco  35946  fneint  36782  fnessref  36791  tailfb  36811  onsucuni3  37935  pibt2  37985  ptrecube  38193  poimirlem4  38197  heicant  38228  mblfinlem1  38230  mblfinlem2  38231  mblfinlem3  38232  mblfinlem4  38233  cnambfre  38241  itg2addnclem2  38245  ftc1anclem5  38270  ftc1anclem6  38271  metf1o  38328  isbnd3b  38358  equivbnd  38363  heiborlem3  38386  rrnmet  38402  rrndstprj1  38403  rrntotbnd  38409  exidcl  38449  ghomco  38464  ghomdiv  38465  grpokerinj  38466  rngoneglmul  38516  rngonegrmul  38517  rngosubdi  38518  rngosubdir  38519  isdrngo2  38531  rngohomco  38547  rngoisocnv  38554  riscer  38561  crngm4  38576  crngohomfo  38579  idlsubcl  38596  inidl  38603  keridl  38605  ispridlc  38643  pridlc3  38646  dmncan1  38649  lflvscl  39775  3dim0  40155  linepsubN  40450  cdlemg2fvlem  41292  trlcoat  41421  istendod  41460  dva1dim  41683  dvhvaddcomN  41794  dihf11  41965  dihlatat  42035  sn-sup2  43189  fsuppssind  43251  mhphf  43255  ismrc  43358  isnacs3  43367  mzpindd  43403  pellex  43488  monotoddzzfi  43595  lermxnn0  43603  rmyeq0  43606  rmyeq  43607  lermy  43608  jm2.27  43661  lsmfgcl  43727  fsumcnsrcl  43819  rngunsnply  43822  gsumws3  44848  mnringmulrcld  44878  nzin  44954  ofdivrec  44962  ofdivcan4  44963  chordthmALT  45567  wessf1ornlem  45829  projf1o  45840  ltdiv23neg  46035  fmulcl  46223  prproropf1olem2  48176  prproropf1olem4  48178  mgmplusgiopALT  48882  itsclc0xyqsolb  49469  toslat  49679  cicerALT  49743