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  6088  fnfco  6707  mpoeq3dva  7446  oprres  7537  fovcdmda  7540  fnmpoovd  8043  offval22  8044  bropfvvvvlem  8047  fnsuppres  8147  suppsssn  8157  sprmpod  8180  oaass  8502  omlimcl  8519  odi  8520  nnmsucr  8566  nnasmo  8604  unfi  9112  ttrclse  9656  cflim2  10192  mulcanenq  10889  mul4  11318  add4  11371  2addsub  11411  addsubeq4  11412  subadd4  11442  muladd  11586  ltleadd  11637  divmul  11816  divne0  11825  div23  11832  div12  11835  div11  11841  divsubdir  11852  subdivcomb1  11853  divcan5  11860  divmuleq  11863  divcan6  11865  divdiv32  11866  div2sub  11983  letrp1  12002  lemul12b  12015  lediv1  12024  lt2mul2div  12037  lemuldiv  12039  ltdiv2  12045  ledivdiv  12048  lediv2  12049  ltdiv23  12050  lediv23  12051  sup2  12115  cju  12158  nndivre  12203  nndivtr  12209  nn0addge1  12464  nn0addge2  12465  peano2uz2  12598  uzind  12602  uzind3  12604  fzind  12608  fnn0ind  12609  uzind4  12841  qre  12888  irrmul  12909  rpdivcl  12954  rerpdivcl  12959  xrinfmsslem  13244  ixxin  13299  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  fzaddel  13495  fzadd2  13496  fzrev  13524  modlt  13818  modcyc  13844  axdc4uzlem  13924  expdiv  14054  fundmge2nop0  14443  swrd00  14585  swrdcl  14586  swrdnnn0nd  14597  swrd0  14599  swrdwrdsymb  14603  ccatpfx  14642  swrdccat  14676  splid  14694  swrdco  14779  2shfti  15022  isermulc2  15600  fsummulc2  15726  dvdscmulr  16230  dvdsmulcr  16231  dvds2add  16236  dvds2sub  16237  dvdstr  16240  alzdvds  16266  divalg2  16351  dvdslegcd  16450  lcmgcdlem  16552  lcmgcdeq  16558  isprm6  16660  pcqcl  16803  vdwmc2  16926  ressinbas  17191  cicer  17748  isposd  18263  pleval2i  18275  poslubmo  18350  posglbmo  18351  tosso  18358  mgmplusf  18559  ismgmd  18561  grpinva  18583  idmgmhm  18610  resmgmhm  18620  resmgmhm2  18621  resmgmhm2b  18622  mgmhmco  18623  mgmhmima  18624  submgmacs  18626  sgrpidmnd  18648  ismndd  18665  imasmnd2  18683  idmhm  18704  mndvcl  18706  issubm2  18713  0mhm  18728  resmhm  18729  resmhm2  18730  resmhm2b  18731  mhmco  18732  mhmimalem  18733  submacs  18736  prdspjmhm  18738  pwsdiagmhm  18740  pwsco1mhm  18741  pwsco2mhm  18742  gsumwsubmcl  18746  gsumsgrpccat  18749  gsumwmhm  18754  grpinvcnv  18920  grpinvnzcl  18925  grpsubf  18933  imasgrp2  18969  qusgrp2  18972  mhmfmhm  18979  mulgnnsubcl  19000  mulgnndir  19017  issubg4  19059  isnsg3  19074  nsgacs  19076  nsgid  19084  qusadd  19102  qus0subgadd  19113  ghmmhm  19140  ghmmhmb  19141  idghm  19145  resghm  19146  ghmf1  19160  qusghm  19169  gaid  19213  subgga  19214  gasubg  19216  invoppggim  19274  gsmsymgrfix  19342  smndlsmidm  19570  pj1ghm  19617  mulgnn0di  19739  mulgmhm  19741  mulgghm  19742  ghmfghm  19744  invghm  19747  ghmplusg  19760  ablnsg  19761  qusabl  19779  gsumval3eu  19818  gsumval3  19821  gsumzcl2  19824  gsumzaddlem  19835  gsumzadd  19836  gsumzmhm  19851  gsumzoppg  19858  srgfcl  20116  srgcom4lem  20133  srgmulgass  20137  srglmhm  20141  srgrmhm  20142  ringcomlem  20199  ringlghm  20232  ringrghm  20233  pwspjmhmmgpd  20248  c0mgm  20379  c0mhm  20380  isnzr2  20438  subrngringnsg  20473  issubrng2  20478  rhmimasubrnglem  20485  issubrg2  20512  domnmuln0  20629  isdomn3  20635  issrngd  20775  islmodd  20804  lmodscaf  20822  lcomf  20839  lmodvsghm  20861  rmodislmodlem  20867  lssacs  20905  idlmhm  20980  invlmhm  20981  lmhmvsca  20984  reslmhm2  20992  reslmhm2b  20993  pwsdiaglmhm  20996  pwssplit2  20999  pwssplit3  21000  issubrgd  21128  qusrhm  21218  qusmul2idl  21221  crngridl  21222  qusmulrng  21224  expmhm  21378  zntoslem  21498  znfld  21502  psgnghm  21522  phlipf  21594  frlmup1  21740  asclghm  21825  asclrhm  21832  rnasclmulcl  21836  psraddcl  21880  psraddclOLD  21881  psrvscacl  21893  psrass23  21911  psrbagev1  22017  coe1sclmulfv  22202  cply1mul  22216  evls1fpws  22289  rhmply1vsca  22308  matbas2d  22343  submaeval  22502  minmar1eval  22569  cpmatacl  22636  pmatcollpw1  22696  pmatcollpw  22701  tgclb  22890  topbas  22892  ntrss  22975  mretopd  23012  neissex  23047  cnpnei  23184  lmcnp  23224  ordthaus  23304  llynlly  23397  restnlly  23402  llyidm  23408  nllyidm  23409  ptbasin  23497  txcnp  23540  ist0-4  23649  kqt0lem  23656  isr0  23657  regr1lem2  23660  cmphmph  23708  connhmph  23709  fbun  23760  trfbas2  23763  isfil2  23776  isfild  23778  infil  23783  fbasfip  23788  fbasrn  23804  trfil2  23807  rnelfmlem  23872  fmfnfmlem3  23876  flimopn  23895  txflf  23926  fclsnei  23939  fclsfnflim  23947  fcfnei  23955  clssubg  24029  tgphaus  24037  qustgplem  24041  tsmsadd  24067  psmetxrge0  24234  psmetlecl  24236  xmetlecl  24267  xmettpos  24270  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  elbl3ps  24312  elbl3  24313  metss  24429  comet  24434  stdbdxmet  24436  stdbdmet  24437  methaus  24441  nrmmetd  24495  abvmet  24496  isngp4  24533  subgngp  24556  nmoi2  24651  nmoleub  24652  nmoid  24663  bl2ioo  24713  zcld  24735  divcnOLD  24790  divcn  24792  divccn  24797  divccnOLD  24799  cncfcdm  24824  divccncf  24832  icoopnst  24869  clmzlmvsca  25046  cph2ass  25146  tcphcph  25170  cfilfcls  25207  bcthlem2  25258  rrxmet  25341  rrxdstprj1  25342  rrxdsfi  25344  cldcss  25374  dvrec  25892  dvmptfsum  25912  aalioulem3  26275  taylply2  26308  taylply2OLD  26309  efsubm  26493  dchrelbasd  27183  dchrmulcl  27193  2sqreulem3  27397  pntrmax  27508  padicabv  27574  nosupbnd2  27661  noinfbnd2  27676  ssltd  27737  divsmulw  28136  axtgcont  28449  xmstrkgc  28866  axsegconlem1  28897  axlowdimlem15  28936  usgredg2vlem1  29205  usgredg2vlem2  29206  iswlkon  29636  wwlksnextsurj  29880  elwwlks2  29946  elwspths2spth  29947  frrusgrord  30320  numclwwlk1lem2foalem  30330  grpoidinvlem2  30484  grpoidinvlem3  30485  ablo4  30529  ablomuldiv  30531  nvaddsub4  30636  nvmeq0  30637  sspmval  30712  sspimsval  30717  lnosub  30738  dipsubdir  30827  hvadd4  31015  hvpncan  31018  his35  31067  hiassdi  31070  shscli  31296  shmodsi  31368  chj4  31514  spansnmul  31543  spansncol  31547  spanunsni  31558  hoadd4  31763  hosubadd4  31793  lnopl  31893  unopf1o  31895  counop  31900  lnfnl  31910  hmopadj2  31920  eighmre  31942  lnopmi  31979  lnophsi  31980  hmops  31999  hmopm  32000  cnlnadjlem2  32047  adjmul  32071  adjadd  32072  kbass6  32100  mdslj1i  32298  mdslj2i  32299  mdslmd1lem1  32304  mdslmd2i  32309  chirredlem3  32371  isoun  32675  xdivmul  32895  odutos  32940  lmodvslmhm  33033  isarchi2  33154  archiabllem2  33166  imasmhm  33318  imasghm  33319  imasrhm  33320  imaslmhm  33321  quslmhm  33323  tngdim  33602  fedgmullem2  33619  metider  33877  pl1cn  33938  rossros  34163  ismeas  34182  dya2iocnei  34266  inelcarsg  34295  signstfvc  34558  bnj563  34726  fisshasheq  35095  cnpconn  35210  cvmseu  35256  elmrsubrn  35500  mrsubco  35501  fneint  36329  fnessref  36338  tailfb  36358  onsucuni3  37348  pibt2  37398  ptrecube  37607  poimirlem4  37611  heicant  37642  mblfinlem1  37644  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  cnambfre  37655  itg2addnclem2  37659  ftc1anclem5  37684  ftc1anclem6  37685  metf1o  37742  isbnd3b  37772  equivbnd  37777  heiborlem3  37800  rrnmet  37816  rrndstprj1  37817  rrntotbnd  37823  exidcl  37863  ghomco  37878  ghomdiv  37879  grpokerinj  37880  rngoneglmul  37930  rngonegrmul  37931  rngosubdi  37932  rngosubdir  37933  isdrngo2  37945  rngohomco  37961  rngoisocnv  37968  riscer  37975  crngm4  37990  crngohomfo  37993  idlsubcl  38010  inidl  38017  keridl  38019  ispridlc  38057  pridlc3  38060  dmncan1  38063  lflvscl  39063  3dim0  39444  linepsubN  39739  cdlemg2fvlem  40581  trlcoat  40710  istendod  40749  dva1dim  40972  dvhvaddcomN  41083  dihf11  41254  dihlatat  41324  sn-sup2  42472  fsuppssind  42574  mhphf  42578  ismrc  42682  isnacs3  42691  mzpindd  42727  pellex  42816  monotoddzzfi  42924  lermxnn0  42932  rmyeq0  42935  rmyeq  42936  lermy  42937  jm2.27  42990  lsmfgcl  43056  fsumcnsrcl  43148  rngunsnply  43151  gsumws3  44178  mnringmulrcld  44210  nzin  44300  ofdivrec  44308  ofdivcan4  44309  chordthmALT  44915  wessf1ornlem  45172  projf1o  45184  ltdiv23neg  45383  fmulcl  45572  prproropf1olem2  47498  prproropf1olem4  47500  mgmplusgiopALT  48175  itsclc0xyqsolb  48752  toslat  48963  cicerALT  49028