Theorem 3expb 1121

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3expia  1122  3adant3r1  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1449  sotri  6129  fnfco  6757  mpoeq3dva  7486  oprres  7575  fovcdmda  7578  fnmpoovd  8073  offval22  8074  bropfvvvvlem  8077  fnsuppres  8176  suppsssn  8186  sprmpod  8209  oaass  8561  omlimcl  8578  odi  8579  nnmsucr  8625  nnasmo  8662  unfi  9172  ttrclse  9722  cflim2  10258  mulcanenq  10955  mul4  11382  add4  11434  2addsub  11474  addsubeq4  11475  subadd4  11504  muladd  11646  ltleadd  11697  divmul  11875  divne0  11884  div23  11891  div12  11894  divsubdir  11908  subdivcomb1  11909  divcan5  11916  divmuleq  11919  divcan6  11921  divdiv32  11922  div2sub  12039  letrp1  12058  lemul12b  12071  lediv1  12079  lt2mul2div  12092  lemuldiv  12094  ltdiv2  12100  ledivdiv  12103  lediv2  12104  ltdiv23  12105  lediv23  12106  sup2  12170  cju  12208  nndivre  12253  nndivtr  12259  nn0addge1  12518  nn0addge2  12519  peano2uz2  12650  uzind  12654  uzind3  12656  fzind  12660  fnn0ind  12661  uzind4  12890  qre  12937  irrmul  12958  rpdivcl  12999  rerpdivcl  13004  xrinfmsslem  13287  ixxin  13341  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  fzaddel  13535  fzadd2  13536  fzrev  13564  modlt  13845  modcyc  13871  axdc4uzlem  13948  expdiv  14079  fundmge2nop0  14453  swrd00  14594  swrdcl  14595  swrdnnn0nd  14606  swrd0  14608  swrdwrdsymb  14612  ccatpfx  14651  swrdccat  14685  splid  14703  swrdco  14788  2shfti  15027  isermulc2  15604  fsummulc2  15730  dvdscmulr  16228  dvdsmulcr  16229  dvds2add  16233  dvds2sub  16234  dvdstr  16237  alzdvds  16263  divalg2  16348  dvdslegcd  16445  lcmgcdlem  16543  lcmgcdeq  16549  isprm6  16651  pcqcl  16789  vdwmc2  16912  ressinbas  17190  cicer  17753  isposd  18276  pleval2i  18289  poslubmo  18364  posglbmo  18365  tosso  18372  mgmplusf  18571  grpinva  18593  sgrpidmnd  18630  ismndd  18647  imasmnd2  18662  idmhm  18681  issubm2  18685  0mhm  18700  resmhm  18701  resmhm2  18702  resmhm2b  18703  mhmco  18704  mhmimalem  18705  submacs  18708  prdspjmhm  18710  pwsdiagmhm  18712  pwsco1mhm  18713  pwsco2mhm  18714  gsumwsubmcl  18718  gsumsgrpccat  18721  gsumwmhm  18726  grpinvcnv  18891  grpinvnzcl  18895  grpsubf  18902  imasgrp2  18938  qusgrp2  18941  mhmfmhm  18948  mulgnnsubcl  18966  mulgnndir  18983  issubg4  19025  isnsg3  19040  nsgacs  19042  nsgid  19050  qusadd  19067  qus0subgadd  19076  ghmmhm  19102  ghmmhmb  19103  idghm  19107  resghm  19108  ghmf1  19121  qusghm  19129  gaid  19163  subgga  19164  gasubg  19166  invoppggim  19227  gsmsymgrfix  19296  smndlsmidm  19524  pj1ghm  19571  mulgnn0di  19693  mulgmhm  19695  mulgghm  19696  ghmfghm  19698  invghm  19701  ghmplusg  19714  ablnsg  19715  qusabl  19733  gsumval3eu  19772  gsumval3  19775  gsumzcl2  19778  gsumzaddlem  19789  gsumzadd  19790  gsumzmhm  19805  gsumzoppg  19812  srgfcl  20019  srgcom4lem  20036  srgmulgass  20040  srglmhm  20044  srgrmhm  20045  ringcomlem  20096  ringlghm  20124  ringrghm  20125  pwspjmhmmgpd  20141  isnzr2  20297  issubrg2  20339  issrngd  20469  islmodd  20477  lmodscaf  20494  lcomf  20511  lmodvsghm  20533  rmodislmodlem  20539  lssacs  20578  idlmhm  20652  invlmhm  20653  lmhmvsca  20656  reslmhm2  20664  reslmhm2b  20665  pwsdiaglmhm  20668  pwssplit2  20671  pwssplit3  20672  issubrgd  20811  qusrhm  20874  qusmul2  20875  crngridl  20876  quscrng  20878  domnmuln0  20914  opprdomn  20919  expmhm  21014  zntoslem  21112  znfld  21116  psgnghm  21133  phlipf  21205  frlmup1  21353  asclghm  21437  asclrhm  21444  rnasclmulcl  21448  psraddcl  21502  psrvscacl  21512  psrass23  21530  psrbagev1  21638  psrbagev1OLD  21639  coe1sclmulfv  21805  cply1mul  21818  mndvcl  21893  matbas2d  21925  submaeval  22084  minmar1eval  22151  cpmatacl  22218  pmatcollpw1  22278  pmatcollpw  22283  tgclb  22473  topbas  22475  ntrss  22559  mretopd  22596  neissex  22631  cnpnei  22768  lmcnp  22808  ordthaus  22888  llynlly  22981  restnlly  22986  llyidm  22992  nllyidm  22993  ptbasin  23081  txcnp  23124  ist0-4  23233  kqt0lem  23240  isr0  23241  regr1lem2  23244  cmphmph  23292  connhmph  23293  fbun  23344  trfbas2  23347  isfil2  23360  isfild  23362  infil  23367  fbasfip  23372  fbasrn  23388  trfil2  23391  rnelfmlem  23456  fmfnfmlem3  23460  flimopn  23479  txflf  23510  fclsnei  23523  fclsfnflim  23531  fcfnei  23539  clssubg  23613  tgphaus  23621  qustgplem  23625  tsmsadd  23651  psmetxrge0  23819  psmetlecl  23821  xmetlecl  23852  xmettpos  23855  imasdsf1olem  23879  imasf1oxmet  23881  imasf1omet  23882  elbl3ps  23897  elbl3  23898  metss  24017  comet  24022  stdbdxmet  24024  stdbdmet  24025  methaus  24029  nrmmetd  24083  abvmet  24084  isngp4  24121  subgngp  24144  nmoi2  24247  nmoleub  24248  nmoid  24259  bl2ioo  24308  zcld  24329  divcn  24384  divccn  24389  cncfcdm  24414  divccncf  24422  icoopnst  24455  clmzlmvsca  24629  cph2ass  24730  tcphcph  24754  cfilfcls  24791  bcthlem2  24842  rrxmet  24925  rrxdstprj1  24926  rrxdsfi  24928  cldcss  24958  dvrec  25472  dvmptfsum  25492  aalioulem3  25847  taylply2  25880  efsubm  26060  dchrelbasd  26742  dchrmulcl  26752  2sqreulem3  26956  pntrmax  27067  padicabv  27133  nosupbnd2  27219  noinfbnd2  27234  ssltd  27293  divsmulw  27640  axtgcont  27720  xmstrkgc  28143  axsegconlem1  28175  axlowdimlem15  28214  usgredg2vlem1  28482  usgredg2vlem2  28483  iswlkon  28914  wwlksnextsurj  29154  elwwlks2  29220  elwspths2spth  29221  frrusgrord  29594  numclwwlk1lem2foalem  29604  grpoidinvlem2  29758  grpoidinvlem3  29759  ablo4  29803  ablomuldiv  29805  nvaddsub4  29910  nvmeq0  29911  sspmval  29986  sspimsval  29991  lnosub  30012  dipsubdir  30101  hvadd4  30289  hvpncan  30292  his35  30341  hiassdi  30344  shscli  30570  shmodsi  30642  chj4  30788  spansnmul  30817  spansncol  30821  spanunsni  30832  hoadd4  31037  hosubadd4  31067  lnopl  31167  unopf1o  31169  counop  31174  lnfnl  31184  hmopadj2  31194  eighmre  31216  lnopmi  31253  lnophsi  31254  hmops  31273  hmopm  31274  cnlnadjlem2  31321  adjmul  31345  adjadd  31346  kbass6  31374  mdslj1i  31572  mdslj2i  31573  mdslmd1lem1  31578  mdslmd2i  31583  chirredlem3  31645  isoun  31923  xdivmul  32091  odutos  32138  lmodvslmhm  32202  isarchi2  32331  archiabllem2  32343  quslmhm  32470  qusmul  32515  evls1fpws  32646  tngdim  32698  fedgmullem2  32715  metider  32874  pl1cn  32935  rossros  33178  ismeas  33197  dya2iocnei  33281  inelcarsg  33310  signstfvc  33585  bnj563  33754  fisshasheq  34104  cnpconn  34221  cvmseu  34267  elmrsubrn  34511  mrsubco  34512  gg-divcn  35163  gg-divccn  35165  fneint  35233  fnessref  35242  tailfb  35262  onsucuni3  36248  pibt2  36298  ptrecube  36488  poimirlem4  36492  heicant  36523  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  cnambfre  36536  itg2addnclem2  36540  ftc1anclem5  36565  ftc1anclem6  36566  metf1o  36623  isbnd3b  36653  equivbnd  36658  heiborlem3  36681  rrnmet  36697  rrndstprj1  36698  rrntotbnd  36704  exidcl  36744  ghomco  36759  ghomdiv  36760  grpokerinj  36761  rngoneglmul  36811  rngonegrmul  36812  rngosubdi  36813  rngosubdir  36814  isdrngo2  36826  rngohomco  36842  rngoisocnv  36849  riscer  36856  crngm4  36871  crngohomfo  36874  idlsubcl  36891  inidl  36898  keridl  36900  ispridlc  36938  pridlc3  36941  dmncan1  36944  lflvscl  37947  3dim0  38328  linepsubN  38623  cdlemg2fvlem  39465  trlcoat  39594  istendod  39633  dva1dim  39856  dvhvaddcomN  39967  dihf11  40138  dihlatat  40208  metakunt12  40996  fsuppssind  41165  mhphf  41169  sn-sup2  41342  ismrc  41439  isnacs3  41448  mzpindd  41484  pellex  41573  monotoddzzfi  41681  lermxnn0  41689  rmyeq0  41692  rmyeq  41693  lermy  41694  jm2.27  41747  lsmfgcl  41816  fsumcnsrcl  41908  rngunsnply  41915  isdomn3  41946  gsumws3  42948  mnringmulrcld  42987  nzin  43077  ofdivrec  43085  ofdivcan4  43086  chordthmALT  43694  wessf1ornlem  43882  projf1o  43896  ltdiv23neg  44104  fmulcl  44297  prproropf1olem2  46172  prproropf1olem4  46174  ismgmd  46546  idmgmhm  46558  resmgmhm  46568  resmgmhm2  46569  resmgmhm2b  46570  mgmhmco  46571  mgmhmima  46572  submgmacs  46574  mgmplusgiopALT  46604  c0mgm  46708  c0mhm  46709  subrngringnsg  46732  issubrng2  46737  rhmimasubrnglem  46744  qusmulrng  46770  itsclc0xyqsolb  47456  toslat  47607