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  6076  fnfco  6689  mpoeq3dva  7426  oprres  7517  fovcdmda  7520  fnmpoovd  8020  offval22  8021  bropfvvvvlem  8024  fnsuppres  8124  suppsssn  8134  sprmpod  8157  oaass  8479  omlimcl  8496  odi  8497  nnmsucr  8543  nnasmo  8581  unfi  9085  ttrclse  9623  cflim2  10157  mulcanenq  10854  mul4  11284  add4  11337  2addsub  11377  addsubeq4  11378  subadd4  11408  muladd  11552  ltleadd  11603  divmul  11782  divne0  11791  div23  11798  div12  11801  div11  11807  divsubdir  11818  subdivcomb1  11819  divcan5  11826  divmuleq  11829  divcan6  11831  divdiv32  11832  div2sub  11949  letrp1  11968  lemul12b  11981  lediv1  11990  lt2mul2div  12003  lemuldiv  12005  ltdiv2  12011  ledivdiv  12014  lediv2  12015  ltdiv23  12016  lediv23  12017  sup2  12081  cju  12124  nndivre  12169  nndivtr  12175  nn0addge1  12430  nn0addge2  12431  peano2uz2  12564  uzind  12568  uzind3  12570  fzind  12574  fnn0ind  12575  uzind4  12807  qre  12854  irrmul  12875  rpdivcl  12920  rerpdivcl  12925  xrinfmsslem  13210  ixxin  13265  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  fzaddel  13461  fzadd2  13462  fzrev  13490  modlt  13784  modcyc  13810  axdc4uzlem  13890  expdiv  14020  fundmge2nop0  14409  swrd00  14551  swrdcl  14552  swrdnnn0nd  14563  swrd0  14565  swrdwrdsymb  14569  ccatpfx  14607  swrdccat  14641  splid  14659  swrdco  14744  2shfti  14987  isermulc2  15565  fsummulc2  15691  dvdscmulr  16195  dvdsmulcr  16196  dvds2add  16201  dvds2sub  16202  dvdstr  16205  alzdvds  16231  divalg2  16316  dvdslegcd  16415  lcmgcdlem  16517  lcmgcdeq  16523  isprm6  16625  pcqcl  16768  vdwmc2  16891  ressinbas  17156  cicer  17713  isposd  18228  pleval2i  18240  poslubmo  18315  posglbmo  18316  tosso  18323  mgmplusf  18524  ismgmd  18526  grpinva  18548  idmgmhm  18575  resmgmhm  18585  resmgmhm2  18586  resmgmhm2b  18587  mgmhmco  18588  mgmhmima  18589  submgmacs  18591  sgrpidmnd  18613  ismndd  18630  imasmnd2  18648  idmhm  18669  mndvcl  18671  issubm2  18678  0mhm  18693  resmhm  18694  resmhm2  18695  resmhm2b  18696  mhmco  18697  mhmimalem  18698  submacs  18701  prdspjmhm  18703  pwsdiagmhm  18705  pwsco1mhm  18706  pwsco2mhm  18707  gsumwsubmcl  18711  gsumsgrpccat  18714  gsumwmhm  18719  grpinvcnv  18885  grpinvnzcl  18890  grpsubf  18898  imasgrp2  18934  qusgrp2  18937  mhmfmhm  18944  mulgnnsubcl  18965  mulgnndir  18982  issubg4  19024  isnsg3  19039  nsgacs  19041  nsgid  19049  qusadd  19067  qus0subgadd  19078  ghmmhm  19105  ghmmhmb  19106  idghm  19110  resghm  19111  ghmf1  19125  qusghm  19134  gaid  19178  subgga  19179  gasubg  19181  invoppggim  19239  gsmsymgrfix  19307  smndlsmidm  19535  pj1ghm  19582  mulgnn0di  19704  mulgmhm  19706  mulgghm  19707  ghmfghm  19709  invghm  19712  ghmplusg  19725  ablnsg  19726  qusabl  19744  gsumval3eu  19783  gsumval3  19786  gsumzcl2  19789  gsumzaddlem  19800  gsumzadd  19801  gsumzmhm  19816  gsumzoppg  19823  srgfcl  20081  srgcom4lem  20098  srgmulgass  20102  srglmhm  20106  srgrmhm  20107  ringcomlem  20164  ringlghm  20197  ringrghm  20198  pwspjmhmmgpd  20213  c0mgm  20344  c0mhm  20345  isnzr2  20403  subrngringnsg  20438  issubrng2  20443  rhmimasubrnglem  20450  issubrg2  20477  domnmuln0  20594  isdomn3  20600  issrngd  20740  islmodd  20769  lmodscaf  20787  lcomf  20804  lmodvsghm  20826  rmodislmodlem  20832  lssacs  20870  idlmhm  20945  invlmhm  20946  lmhmvsca  20949  reslmhm2  20957  reslmhm2b  20958  pwsdiaglmhm  20961  pwssplit2  20964  pwssplit3  20965  issubrgd  21093  qusrhm  21183  qusmul2idl  21186  crngridl  21187  qusmulrng  21189  expmhm  21343  zntoslem  21463  znfld  21467  psgnghm  21487  phlipf  21559  frlmup1  21705  asclghm  21790  asclrhm  21797  rnasclmulcl  21801  psraddcl  21845  psraddclOLD  21846  psrvscacl  21858  psrass23  21876  psrbagev1  21982  coe1sclmulfv  22167  cply1mul  22181  evls1fpws  22254  rhmply1vsca  22273  matbas2d  22308  submaeval  22467  minmar1eval  22534  cpmatacl  22601  pmatcollpw1  22661  pmatcollpw  22666  tgclb  22855  topbas  22857  ntrss  22940  mretopd  22977  neissex  23012  cnpnei  23149  lmcnp  23189  ordthaus  23269  llynlly  23362  restnlly  23367  llyidm  23373  nllyidm  23374  ptbasin  23462  txcnp  23505  ist0-4  23614  kqt0lem  23621  isr0  23622  regr1lem2  23625  cmphmph  23673  connhmph  23674  fbun  23725  trfbas2  23728  isfil2  23741  isfild  23743  infil  23748  fbasfip  23753  fbasrn  23769  trfil2  23772  rnelfmlem  23837  fmfnfmlem3  23841  flimopn  23860  txflf  23891  fclsnei  23904  fclsfnflim  23912  fcfnei  23920  clssubg  23994  tgphaus  24002  qustgplem  24006  tsmsadd  24032  psmetxrge0  24199  psmetlecl  24201  xmetlecl  24232  xmettpos  24235  imasdsf1olem  24259  imasf1oxmet  24261  imasf1omet  24262  elbl3ps  24277  elbl3  24278  metss  24394  comet  24399  stdbdxmet  24401  stdbdmet  24402  methaus  24406  nrmmetd  24460  abvmet  24461  isngp4  24498  subgngp  24521  nmoi2  24616  nmoleub  24617  nmoid  24628  bl2ioo  24678  zcld  24700  divcnOLD  24755  divcn  24757  divccn  24762  divccnOLD  24764  cncfcdm  24789  divccncf  24797  icoopnst  24834  clmzlmvsca  25011  cph2ass  25111  tcphcph  25135  cfilfcls  25172  bcthlem2  25223  rrxmet  25306  rrxdstprj1  25307  rrxdsfi  25309  cldcss  25339  dvrec  25857  dvmptfsum  25877  aalioulem3  26240  taylply2  26273  taylply2OLD  26274  efsubm  26458  dchrelbasd  27148  dchrmulcl  27158  2sqreulem3  27362  pntrmax  27473  padicabv  27539  nosupbnd2  27626  noinfbnd2  27641  ssltd  27702  divsmulw  28101  axtgcont  28414  xmstrkgc  28831  axsegconlem1  28862  axlowdimlem15  28901  usgredg2vlem1  29170  usgredg2vlem2  29171  iswlkon  29601  wwlksnextsurj  29845  elwwlks2  29911  elwspths2spth  29912  frrusgrord  30285  numclwwlk1lem2foalem  30295  grpoidinvlem2  30449  grpoidinvlem3  30450  ablo4  30494  ablomuldiv  30496  nvaddsub4  30601  nvmeq0  30602  sspmval  30677  sspimsval  30682  lnosub  30703  dipsubdir  30792  hvadd4  30980  hvpncan  30983  his35  31032  hiassdi  31035  shscli  31261  shmodsi  31333  chj4  31479  spansnmul  31508  spansncol  31512  spanunsni  31523  hoadd4  31728  hosubadd4  31758  lnopl  31858  unopf1o  31860  counop  31865  lnfnl  31875  hmopadj2  31885  eighmre  31907  lnopmi  31944  lnophsi  31945  hmops  31964  hmopm  31965  cnlnadjlem2  32012  adjmul  32036  adjadd  32037  kbass6  32065  mdslj1i  32263  mdslj2i  32264  mdslmd1lem1  32269  mdslmd2i  32274  chirredlem3  32336  isoun  32645  xdivmul  32866  odutos  32911  lmodvslmhm  33004  isarchi2  33128  archiabllem2  33140  imasmhm  33292  imasghm  33293  imasrhm  33294  imaslmhm  33295  quslmhm  33297  tngdim  33586  fedgmullem2  33603  metider  33867  pl1cn  33928  rossros  34153  ismeas  34172  dya2iocnei  34256  inelcarsg  34285  signstfvc  34548  bnj563  34716  fisshasheq  35098  cnpconn  35213  cvmseu  35259  elmrsubrn  35503  mrsubco  35504  fneint  36332  fnessref  36341  tailfb  36361  onsucuni3  37351  pibt2  37401  ptrecube  37610  poimirlem4  37614  heicant  37645  mblfinlem1  37647  mblfinlem2  37648  mblfinlem3  37649  mblfinlem4  37650  cnambfre  37658  itg2addnclem2  37662  ftc1anclem5  37687  ftc1anclem6  37688  metf1o  37745  isbnd3b  37775  equivbnd  37780  heiborlem3  37803  rrnmet  37819  rrndstprj1  37820  rrntotbnd  37826  exidcl  37866  ghomco  37881  ghomdiv  37882  grpokerinj  37883  rngoneglmul  37933  rngonegrmul  37934  rngosubdi  37935  rngosubdir  37936  isdrngo2  37948  rngohomco  37964  rngoisocnv  37971  riscer  37978  crngm4  37993  crngohomfo  37996  idlsubcl  38013  inidl  38020  keridl  38022  ispridlc  38060  pridlc3  38063  dmncan1  38066  lflvscl  39066  3dim0  39446  linepsubN  39741  cdlemg2fvlem  40583  trlcoat  40712  istendod  40751  dva1dim  40974  dvhvaddcomN  41085  dihf11  41256  dihlatat  41326  sn-sup2  42474  fsuppssind  42576  mhphf  42580  ismrc  42684  isnacs3  42693  mzpindd  42729  pellex  42818  monotoddzzfi  42925  lermxnn0  42933  rmyeq0  42936  rmyeq  42937  lermy  42938  jm2.27  42991  lsmfgcl  43057  fsumcnsrcl  43149  rngunsnply  43152  gsumws3  44179  mnringmulrcld  44211  nzin  44301  ofdivrec  44309  ofdivcan4  44310  chordthmALT  44916  wessf1ornlem  45173  projf1o  45185  ltdiv23neg  45383  fmulcl  45572  prproropf1olem2  47498  prproropf1olem4  47500  mgmplusgiopALT  48188  itsclc0xyqsolb  48765  toslat  48976  cicerALT  49041