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 1087

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 1089

This theorem is referenced by:  3expia  1121  3adant3r1  1182  3adant3r2  1183  3adant3r3  1184  mp3an1  1448  sotri  6159  fnfco  6786  mpoeq3dva  7527  oprres  7618  fovcdmda  7621  fnmpoovd  8128  offval22  8129  bropfvvvvlem  8132  fnsuppres  8232  suppsssn  8242  sprmpod  8265  oaass  8617  omlimcl  8634  odi  8635  nnmsucr  8681  nnasmo  8719  unfi  9238  ttrclse  9796  cflim2  10332  mulcanenq  11029  mul4  11458  add4  11510  2addsub  11550  addsubeq4  11551  subadd4  11580  muladd  11722  ltleadd  11773  divmul  11952  divne0  11961  div23  11968  div12  11971  div11  11977  divsubdir  11988  subdivcomb1  11989  divcan5  11996  divmuleq  11999  divcan6  12001  divdiv32  12002  div2sub  12119  letrp1  12138  lemul12b  12151  lediv1  12160  lt2mul2div  12173  lemuldiv  12175  ltdiv2  12181  ledivdiv  12184  lediv2  12185  ltdiv23  12186  lediv23  12187  sup2  12251  cju  12289  nndivre  12334  nndivtr  12340  nn0addge1  12599  nn0addge2  12600  peano2uz2  12731  uzind  12735  uzind3  12737  fzind  12741  fnn0ind  12742  uzind4  12971  qre  13018  irrmul  13039  rpdivcl  13082  rerpdivcl  13087  xrinfmsslem  13370  ixxin  13424  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzaddel  13618  fzadd2  13619  fzrev  13647  modlt  13931  modcyc  13957  axdc4uzlem  14034  expdiv  14164  fundmge2nop0  14551  swrd00  14692  swrdcl  14693  swrdnnn0nd  14704  swrd0  14706  swrdwrdsymb  14710  ccatpfx  14749  swrdccat  14783  splid  14801  swrdco  14886  2shfti  15129  isermulc2  15706  fsummulc2  15832  dvdscmulr  16333  dvdsmulcr  16334  dvds2add  16338  dvds2sub  16339  dvdstr  16342  alzdvds  16368  divalg2  16453  dvdslegcd  16550  lcmgcdlem  16653  lcmgcdeq  16659  isprm6  16761  pcqcl  16903  vdwmc2  17026  ressinbas  17304  cicer  17867  isposd  18393  pleval2i  18406  poslubmo  18481  posglbmo  18482  tosso  18489  mgmplusf  18688  ismgmd  18690  grpinva  18712  idmgmhm  18739  resmgmhm  18749  resmgmhm2  18750  resmgmhm2b  18751  mgmhmco  18752  mgmhmima  18753  submgmacs  18755  sgrpidmnd  18777  ismndd  18794  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  19046  grpinvnzcl  19051  grpsubf  19059  imasgrp2  19095  qusgrp2  19098  mhmfmhm  19105  mulgnnsubcl  19126  mulgnndir  19143  issubg4  19185  isnsg3  19200  nsgacs  19202  nsgid  19210  qusadd  19228  qus0subgadd  19239  ghmmhm  19266  ghmmhmb  19267  idghm  19271  resghm  19272  ghmf1  19286  qusghm  19295  gaid  19339  subgga  19340  gasubg  19342  invoppggim  19403  gsmsymgrfix  19470  smndlsmidm  19698  pj1ghm  19745  mulgnn0di  19867  mulgmhm  19869  mulgghm  19870  ghmfghm  19872  invghm  19875  ghmplusg  19888  ablnsg  19889  qusabl  19907  gsumval3eu  19946  gsumval3  19949  gsumzcl2  19952  gsumzaddlem  19963  gsumzadd  19964  gsumzmhm  19979  gsumzoppg  19986  srgfcl  20223  srgcom4lem  20240  srgmulgass  20244  srglmhm  20248  srgrmhm  20249  ringcomlem  20302  ringlghm  20335  ringrghm  20336  pwspjmhmmgpd  20351  c0mgm  20485  c0mhm  20486  isnzr2  20544  subrngringnsg  20579  issubrng2  20584  rhmimasubrnglem  20591  issubrg2  20620  domnmuln0  20731  isdomn3  20737  issrngd  20878  islmodd  20886  lmodscaf  20904  lcomf  20921  lmodvsghm  20943  rmodislmodlem  20949  lssacs  20988  idlmhm  21063  invlmhm  21064  lmhmvsca  21067  reslmhm2  21075  reslmhm2b  21076  pwsdiaglmhm  21079  pwssplit2  21082  pwssplit3  21083  issubrgd  21219  qusrhm  21309  qusmul2idl  21312  crngridl  21313  qusmulrng  21315  expmhm  21477  zntoslem  21598  znfld  21602  psgnghm  21621  phlipf  21693  frlmup1  21841  asclghm  21926  asclrhm  21933  rnasclmulcl  21937  psraddcl  21981  psraddclOLD  21982  psrvscacl  21994  psrass23  22012  psrbagev1  22124  coe1sclmulfv  22307  cply1mul  22321  evls1fpws  22394  rhmply1vsca  22413  matbas2d  22450  submaeval  22609  minmar1eval  22676  cpmatacl  22743  pmatcollpw1  22803  pmatcollpw  22808  tgclb  22998  topbas  23000  ntrss  23084  mretopd  23121  neissex  23156  cnpnei  23293  lmcnp  23333  ordthaus  23413  llynlly  23506  restnlly  23511  llyidm  23517  nllyidm  23518  ptbasin  23606  txcnp  23649  ist0-4  23758  kqt0lem  23765  isr0  23766  regr1lem2  23769  cmphmph  23817  connhmph  23818  fbun  23869  trfbas2  23872  isfil2  23885  isfild  23887  infil  23892  fbasfip  23897  fbasrn  23913  trfil2  23916  rnelfmlem  23981  fmfnfmlem3  23985  flimopn  24004  txflf  24035  fclsnei  24048  fclsfnflim  24056  fcfnei  24064  clssubg  24138  tgphaus  24146  qustgplem  24150  tsmsadd  24176  psmetxrge0  24344  psmetlecl  24346  xmetlecl  24377  xmettpos  24380  imasdsf1olem  24404  imasf1oxmet  24406  imasf1omet  24407  elbl3ps  24422  elbl3  24423  metss  24542  comet  24547  stdbdxmet  24549  stdbdmet  24550  methaus  24554  nrmmetd  24608  abvmet  24609  isngp4  24646  subgngp  24669  nmoi2  24772  nmoleub  24773  nmoid  24784  bl2ioo  24833  zcld  24854  divcnOLD  24909  divcn  24911  divccn  24916  divccnOLD  24918  cncfcdm  24943  divccncf  24951  icoopnst  24988  clmzlmvsca  25165  cph2ass  25266  tcphcph  25290  cfilfcls  25327  bcthlem2  25378  rrxmet  25461  rrxdstprj1  25462  rrxdsfi  25464  cldcss  25494  dvrec  26013  dvmptfsum  26033  aalioulem3  26394  taylply2  26427  taylply2OLD  26428  efsubm  26611  dchrelbasd  27301  dchrmulcl  27311  2sqreulem3  27515  pntrmax  27626  padicabv  27692  nosupbnd2  27779  noinfbnd2  27794  ssltd  27854  divsmulw  28236  axtgcont  28495  xmstrkgc  28918  axsegconlem1  28950  axlowdimlem15  28989  usgredg2vlem1  29260  usgredg2vlem2  29261  iswlkon  29693  wwlksnextsurj  29933  elwwlks2  29999  elwspths2spth  30000  frrusgrord  30373  numclwwlk1lem2foalem  30383  grpoidinvlem2  30537  grpoidinvlem3  30538  ablo4  30582  ablomuldiv  30584  nvaddsub4  30689  nvmeq0  30690  sspmval  30765  sspimsval  30770  lnosub  30791  dipsubdir  30880  hvadd4  31068  hvpncan  31071  his35  31120  hiassdi  31123  shscli  31349  shmodsi  31421  chj4  31567  spansnmul  31596  spansncol  31600  spanunsni  31611  hoadd4  31816  hosubadd4  31846  lnopl  31946  unopf1o  31948  counop  31953  lnfnl  31963  hmopadj2  31973  eighmre  31995  lnopmi  32032  lnophsi  32033  hmops  32052  hmopm  32053  cnlnadjlem2  32100  adjmul  32124  adjadd  32125  kbass6  32153  mdslj1i  32351  mdslj2i  32352  mdslmd1lem1  32357  mdslmd2i  32362  chirredlem3  32424  isoun  32713  xdivmul  32889  odutos  32941  lmodvslmhm  33033  isarchi2  33165  archiabllem2  33177  imasmhm  33347  imasghm  33348  imasrhm  33349  imaslmhm  33350  quslmhm  33352  tngdim  33626  fedgmullem2  33643  metider  33840  pl1cn  33901  rossros  34144  ismeas  34163  dya2iocnei  34247  inelcarsg  34276  signstfvc  34551  bnj563  34719  fisshasheq  35082  cnpconn  35198  cvmseu  35244  elmrsubrn  35488  mrsubco  35489  fneint  36314  fnessref  36323  tailfb  36343  onsucuni3  37333  pibt2  37383  ptrecube  37580  poimirlem4  37584  heicant  37615  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  cnambfre  37628  itg2addnclem2  37632  ftc1anclem5  37657  ftc1anclem6  37658  metf1o  37715  isbnd3b  37745  equivbnd  37750  heiborlem3  37773  rrnmet  37789  rrndstprj1  37790  rrntotbnd  37796  exidcl  37836  ghomco  37851  ghomdiv  37852  grpokerinj  37853  rngoneglmul  37903  rngonegrmul  37904  rngosubdi  37905  rngosubdir  37906  isdrngo2  37918  rngohomco  37934  rngoisocnv  37941  riscer  37948  crngm4  37963  crngohomfo  37966  idlsubcl  37983  inidl  37990  keridl  37992  ispridlc  38030  pridlc3  38033  dmncan1  38036  lflvscl  39033  3dim0  39414  linepsubN  39709  cdlemg2fvlem  40551  trlcoat  40680  istendod  40719  dva1dim  40942  dvhvaddcomN  41053  dihf11  41224  dihlatat  41294  metakunt12  42173  sn-sup2  42447  fsuppssind  42548  mhphf  42552  ismrc  42657  isnacs3  42666  mzpindd  42702  pellex  42791  monotoddzzfi  42899  lermxnn0  42907  rmyeq0  42910  rmyeq  42911  lermy  42912  jm2.27  42965  lsmfgcl  43031  fsumcnsrcl  43123  rngunsnply  43130  gsumws3  44158  mnringmulrcld  44197  nzin  44287  ofdivrec  44295  ofdivcan4  44296  chordthmALT  44904  wessf1ornlem  45092  projf1o  45104  ltdiv23neg  45309  fmulcl  45502  prproropf1olem2  47378  prproropf1olem4  47380  mgmplusgiopALT  47917  itsclc0xyqsolb  48504  toslat  48654