Theorem 3expb 1120

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3expia  1121  3adant3r1  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1450  sotri  6121  fnfco  6748  mpoeq3dva  7489  oprres  7580  fovcdmda  7583  fnmpoovd  8091  offval22  8092  bropfvvvvlem  8095  fnsuppres  8195  suppsssn  8205  sprmpod  8228  oaass  8578  omlimcl  8595  odi  8596  nnmsucr  8642  nnasmo  8680  unfi  9190  ttrclse  9746  cflim2  10282  mulcanenq  10979  mul4  11408  add4  11461  2addsub  11501  addsubeq4  11502  subadd4  11532  muladd  11674  ltleadd  11725  divmul  11904  divne0  11913  div23  11920  div12  11923  div11  11929  divsubdir  11940  subdivcomb1  11941  divcan5  11948  divmuleq  11951  divcan6  11953  divdiv32  11954  div2sub  12071  letrp1  12090  lemul12b  12103  lediv1  12112  lt2mul2div  12125  lemuldiv  12127  ltdiv2  12133  ledivdiv  12136  lediv2  12137  ltdiv23  12138  lediv23  12139  sup2  12203  cju  12241  nndivre  12286  nndivtr  12292  nn0addge1  12552  nn0addge2  12553  peano2uz2  12686  uzind  12690  uzind3  12692  fzind  12696  fnn0ind  12697  uzind4  12927  qre  12974  irrmul  12995  rpdivcl  13039  rerpdivcl  13044  xrinfmsslem  13329  ixxin  13384  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  fzaddel  13580  fzadd2  13581  fzrev  13609  modlt  13902  modcyc  13928  axdc4uzlem  14006  expdiv  14136  fundmge2nop0  14525  swrd00  14667  swrdcl  14668  swrdnnn0nd  14679  swrd0  14681  swrdwrdsymb  14685  ccatpfx  14724  swrdccat  14758  splid  14776  swrdco  14861  2shfti  15104  isermulc2  15679  fsummulc2  15805  dvdscmulr  16309  dvdsmulcr  16310  dvds2add  16314  dvds2sub  16315  dvdstr  16318  alzdvds  16344  divalg2  16429  dvdslegcd  16528  lcmgcdlem  16630  lcmgcdeq  16636  isprm6  16738  pcqcl  16881  vdwmc2  17004  ressinbas  17271  cicer  17824  isposd  18339  pleval2i  18351  poslubmo  18426  posglbmo  18427  tosso  18434  mgmplusf  18633  ismgmd  18635  grpinva  18657  idmgmhm  18684  resmgmhm  18694  resmgmhm2  18695  resmgmhm2b  18696  mgmhmco  18697  mgmhmima  18698  submgmacs  18700  sgrpidmnd  18722  ismndd  18739  imasmnd2  18757  idmhm  18778  mndvcl  18780  issubm2  18787  0mhm  18802  resmhm  18803  resmhm2  18804  resmhm2b  18805  mhmco  18806  mhmimalem  18807  submacs  18810  prdspjmhm  18812  pwsdiagmhm  18814  pwsco1mhm  18815  pwsco2mhm  18816  gsumwsubmcl  18820  gsumsgrpccat  18823  gsumwmhm  18828  grpinvcnv  18994  grpinvnzcl  18999  grpsubf  19007  imasgrp2  19043  qusgrp2  19046  mhmfmhm  19053  mulgnnsubcl  19074  mulgnndir  19091  issubg4  19133  isnsg3  19148  nsgacs  19150  nsgid  19158  qusadd  19176  qus0subgadd  19187  ghmmhm  19214  ghmmhmb  19215  idghm  19219  resghm  19220  ghmf1  19234  qusghm  19243  gaid  19287  subgga  19288  gasubg  19290  invoppggim  19348  gsmsymgrfix  19414  smndlsmidm  19642  pj1ghm  19689  mulgnn0di  19811  mulgmhm  19813  mulgghm  19814  ghmfghm  19816  invghm  19819  ghmplusg  19832  ablnsg  19833  qusabl  19851  gsumval3eu  19890  gsumval3  19893  gsumzcl2  19896  gsumzaddlem  19907  gsumzadd  19908  gsumzmhm  19923  gsumzoppg  19930  srgfcl  20161  srgcom4lem  20178  srgmulgass  20182  srglmhm  20186  srgrmhm  20187  ringcomlem  20244  ringlghm  20277  ringrghm  20278  pwspjmhmmgpd  20293  c0mgm  20424  c0mhm  20425  isnzr2  20483  subrngringnsg  20518  issubrng2  20523  rhmimasubrnglem  20530  issubrg2  20557  domnmuln0  20674  isdomn3  20680  issrngd  20820  islmodd  20828  lmodscaf  20846  lcomf  20863  lmodvsghm  20885  rmodislmodlem  20891  lssacs  20929  idlmhm  21004  invlmhm  21005  lmhmvsca  21008  reslmhm2  21016  reslmhm2b  21017  pwsdiaglmhm  21020  pwssplit2  21023  pwssplit3  21024  issubrgd  21152  qusrhm  21242  qusmul2idl  21245  crngridl  21246  qusmulrng  21248  expmhm  21409  zntoslem  21522  znfld  21526  psgnghm  21545  phlipf  21617  frlmup1  21763  asclghm  21848  asclrhm  21855  rnasclmulcl  21859  psraddcl  21903  psraddclOLD  21904  psrvscacl  21916  psrass23  21934  psrbagev1  22040  coe1sclmulfv  22225  cply1mul  22239  evls1fpws  22312  rhmply1vsca  22331  matbas2d  22366  submaeval  22525  minmar1eval  22592  cpmatacl  22659  pmatcollpw1  22719  pmatcollpw  22724  tgclb  22913  topbas  22915  ntrss  22998  mretopd  23035  neissex  23070  cnpnei  23207  lmcnp  23247  ordthaus  23327  llynlly  23420  restnlly  23425  llyidm  23431  nllyidm  23432  ptbasin  23520  txcnp  23563  ist0-4  23672  kqt0lem  23679  isr0  23680  regr1lem2  23683  cmphmph  23731  connhmph  23732  fbun  23783  trfbas2  23786  isfil2  23799  isfild  23801  infil  23806  fbasfip  23811  fbasrn  23827  trfil2  23830  rnelfmlem  23895  fmfnfmlem3  23899  flimopn  23918  txflf  23949  fclsnei  23962  fclsfnflim  23970  fcfnei  23978  clssubg  24052  tgphaus  24060  qustgplem  24064  tsmsadd  24090  psmetxrge0  24257  psmetlecl  24259  xmetlecl  24290  xmettpos  24293  imasdsf1olem  24317  imasf1oxmet  24319  imasf1omet  24320  elbl3ps  24335  elbl3  24336  metss  24452  comet  24457  stdbdxmet  24459  stdbdmet  24460  methaus  24464  nrmmetd  24518  abvmet  24519  isngp4  24556  subgngp  24579  nmoi2  24674  nmoleub  24675  nmoid  24686  bl2ioo  24736  zcld  24758  divcnOLD  24813  divcn  24815  divccn  24820  divccnOLD  24822  cncfcdm  24847  divccncf  24855  icoopnst  24892  clmzlmvsca  25069  cph2ass  25170  tcphcph  25194  cfilfcls  25231  bcthlem2  25282  rrxmet  25365  rrxdstprj1  25366  rrxdsfi  25368  cldcss  25398  dvrec  25916  dvmptfsum  25936  aalioulem3  26299  taylply2  26332  taylply2OLD  26333  efsubm  26517  dchrelbasd  27207  dchrmulcl  27217  2sqreulem3  27421  pntrmax  27532  padicabv  27598  nosupbnd2  27685  noinfbnd2  27700  ssltd  27760  divsmulw  28153  axtgcont  28453  xmstrkgc  28870  axsegconlem1  28901  axlowdimlem15  28940  usgredg2vlem1  29209  usgredg2vlem2  29210  iswlkon  29642  wwlksnextsurj  29887  elwwlks2  29953  elwspths2spth  29954  frrusgrord  30327  numclwwlk1lem2foalem  30337  grpoidinvlem2  30491  grpoidinvlem3  30492  ablo4  30536  ablomuldiv  30538  nvaddsub4  30643  nvmeq0  30644  sspmval  30719  sspimsval  30724  lnosub  30745  dipsubdir  30834  hvadd4  31022  hvpncan  31025  his35  31074  hiassdi  31077  shscli  31303  shmodsi  31375  chj4  31521  spansnmul  31550  spansncol  31554  spanunsni  31565  hoadd4  31770  hosubadd4  31800  lnopl  31900  unopf1o  31902  counop  31907  lnfnl  31917  hmopadj2  31927  eighmre  31949  lnopmi  31986  lnophsi  31987  hmops  32006  hmopm  32007  cnlnadjlem2  32054  adjmul  32078  adjadd  32079  kbass6  32107  mdslj1i  32305  mdslj2i  32306  mdslmd1lem1  32311  mdslmd2i  32316  chirredlem3  32378  isoun  32684  xdivmul  32904  odutos  32953  lmodvslmhm  33049  isarchi2  33188  archiabllem2  33200  imasmhm  33374  imasghm  33375  imasrhm  33376  imaslmhm  33377  quslmhm  33379  tngdim  33658  fedgmullem2  33675  metider  33930  pl1cn  33991  rossros  34216  ismeas  34235  dya2iocnei  34319  inelcarsg  34348  signstfvc  34611  bnj563  34779  fisshasheq  35142  cnpconn  35257  cvmseu  35303  elmrsubrn  35547  mrsubco  35548  fneint  36371  fnessref  36380  tailfb  36400  onsucuni3  37390  pibt2  37440  ptrecube  37649  poimirlem4  37653  heicant  37684  mblfinlem1  37686  mblfinlem2  37687  mblfinlem3  37688  mblfinlem4  37689  cnambfre  37697  itg2addnclem2  37701  ftc1anclem5  37726  ftc1anclem6  37727  metf1o  37784  isbnd3b  37814  equivbnd  37819  heiborlem3  37842  rrnmet  37858  rrndstprj1  37859  rrntotbnd  37865  exidcl  37905  ghomco  37920  ghomdiv  37921  grpokerinj  37922  rngoneglmul  37972  rngonegrmul  37973  rngosubdi  37974  rngosubdir  37975  isdrngo2  37987  rngohomco  38003  rngoisocnv  38010  riscer  38017  crngm4  38032  crngohomfo  38035  idlsubcl  38052  inidl  38059  keridl  38061  ispridlc  38099  pridlc3  38102  dmncan1  38105  lflvscl  39100  3dim0  39481  linepsubN  39776  cdlemg2fvlem  40618  trlcoat  40747  istendod  40786  dva1dim  41009  dvhvaddcomN  41120  dihf11  41291  dihlatat  41361  sn-sup2  42489  fsuppssind  42591  mhphf  42595  ismrc  42699  isnacs3  42708  mzpindd  42744  pellex  42833  monotoddzzfi  42941  lermxnn0  42949  rmyeq0  42952  rmyeq  42953  lermy  42954  jm2.27  43007  lsmfgcl  43073  fsumcnsrcl  43165  rngunsnply  43168  gsumws3  44195  mnringmulrcld  44227  nzin  44317  ofdivrec  44325  ofdivcan4  44326  chordthmALT  44932  wessf1ornlem  45189  projf1o  45201  ltdiv23neg  45401  fmulcl  45590  prproropf1olem2  47498  prproropf1olem4  47500  mgmplusgiopALT  48149  itsclc0xyqsolb  48730  toslat  48936  cicerALT  48993