Theorem 3expb 1138

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expia  1139  3adant3r1  1201  3adant3r2  1202  3adant3r3  1203  mp3an1  1477  sotri  6127  fnfco  6758  mpoeq3dva  7507  oprres  7598  fovcdmda  7602  fnmpoovd  8109  offval22  8110  bropfvvvvlem  8113  fnsuppres  8222  suppsssn  8232  sprmpod  8255  oaass  8583  omlimcl  8600  odi  8601  nnmsucr  8648  nnasmo  8686  unfi  9200  ttrclse  9741  cflim2  10354  mulcanenq  11058  mul4  11491  add4  11544  2addsub  11584  addsubeq4  11585  subadd4  11615  muladd  11761  ltleadd  11812  divmul  11990  divne0  11999  div23  12006  div12  12009  div11  12015  divsubdir  12023  subdivcomb1  12025  divcan5  12032  divmuleq  12035  divcan6  12037  divdiv32  12038  div2sub  12155  letrp1  12174  lemul12b  12187  lediv1  12195  lt2mul2div  12208  lemuldiv  12210  ltdiv2  12216  ledivdiv  12219  lediv2  12220  ltdiv23  12221  lediv23  12222  sup2  12286  cju  12329  nndivre  12392  nndivtr  12398  nn0addge1  12665  nn0addge2  12666  peano2uz2  12800  uzind  12804  uzind3  12806  fzind  12810  fnn0ind  12811  uzind4  13046  qre  13093  irrmul  13115  rpdivcl  13160  rerpdivcl  13165  xrinfmsslem  13451  ixxin  13506  iccshftr  13630  iccshftl  13632  iccdil  13634  icccntr  13636  fzaddel  13705  fzadd2  13706  fzrev  13734  modlt  14033  modcyc  14059  axdc4uzlem  14139  expdiv  14269  fundmge2nop0  14660  swrd00  14806  swrdcl  14807  swrdnnn0nd  14820  swrd0  14822  swrdwrdsymb  14826  ccatpfx  14864  swrdccat  14898  splid  14916  swrdco  15002  2shfti  15248  isermulc2  15840  fsummulc2  15965  dvdscmulr  16469  dvdsmulcr  16470  dvds2add  16475  dvds2sub  16476  dvdstr  16479  alzdvds  16505  divalg2  16590  dvdslegcd  16689  lcmgcdlem  16796  lcmgcdeq  16802  isprm6  16905  pcqcl  17049  vdwmc2  17172  ressinbas  17438  cicer  17996  isposd  18511  pleval2i  18523  poslubmo  18598  posglbmo  18599  tosso  18606  mgmplusf  18841  mgmn0plusgf  18842  ismgmd  18845  grpinva  18870  imasmgm2  18878  qusmgm  18879  idmgmhm  18905  resmgmhm  18915  resmgmhm2  18916  resmgmhm2b  18917  mgmhmco  18918  mgmhmima  18919  submgmacs  18921  ismndd  18961  imasmnd2  18983  qusmnd  18990  idmhm  19005  mndvcl  19007  issubm2  19014  0mhm  19030  resmhm  19031  resmhm2  19032  resmhm2b  19033  mhmco  19034  mhmimalem  19035  submacs  19038  prdspjmhm  19040  pwsdiagmhm  19042  pwsco1mhm  19043  pwsco2mhm  19044  gsumwsubmcl  19048  gsumsgrpccat  19051  gsumwmhm  19056  grpinvcnv  19232  grpinvnzcl  19236  grpsubf  19244  imasgrp2  19280  qusgrp2  19283  mhmfmhm  19290  mulgnnsubcl  19311  mulgnndir  19328  issubg4  19371  isnsg3  19385  nsgacs  19387  nsgid  19395  qusadd  19418  qus0subgadd  19429  ghmmhm  19455  ghmmhmb  19456  idghm  19460  resghm  19461  ghmf1  19475  qusghm  19484  gaid  19528  subgga  19529  gasubg  19531  invoppggim  19589  gsmsymgrfix  19657  smndlsmidm  19885  pj1ghm  19932  mulgnn0di  20054  mulgmhm  20056  mulgghm  20057  ghmfghm  20059  invghm  20062  ghmplusg  20075  ablnsg  20076  qusabl  20094  gsumval3eu  20133  gsumval3  20136  gsumzcl2  20139  gsumzaddlem  20150  gsumzadd  20151  gsumzmhm  20166  gsumzoppg  20173  srgfcl  20437  srgcom4lem  20454  srgmulgass  20458  srglmhm  20462  srgrmhm  20463  ringcomlem  20523  ringlghm  20558  ringrghm  20559  pwspjmhmmgpd  20572  c0mgm  20704  c0mhm  20705  isnzr2  20783  subrngringnsg  20820  issubrng2  20825  rhmimasubrnglem  20832  issubrg2  20859  domnmuln0  20976  isdomn3  20981  isdrng3lem2  21021  issrngd  21127  islmodd  21156  lmodscaf  21174  lcomf  21191  lmodvsghm  21213  rmodislmodlem  21219  lssacs  21257  idlmhm  21331  invlmhm  21332  lmhmvsca  21335  reslmhm2  21343  reslmhm2b  21344  pwsdiaglmhm  21347  pwssplit2  21350  pwssplit3  21351  issubrgd  21479  qusrhm  21585  qusmul2idl  21589  crngridl  21590  qusmulrng  21593  cmprmidlmcl  21646  expmhm  21757  zntoslem  21877  znfld  21881  psgnghm  21901  phlipf  21973  frlmup1  22119  asclghm  22205  asclrhm  22213  rnasclmulcl  22217  psraddcl  22262  psrvscacl  22274  psrass23  22291  psrbagev1  22401  coe1sclmulfv  22617  cply1mul  22629  evls1fpws  22702  rhmply1vsca  22718  matbas2d  22753  submaeval  22912  minmar1eval  22979  cpmatacl  23049  pmatcollpw1  23109  pmatcollpw  23114  tgclb  23303  topbas  23305  ntrss  23388  mretopd  23425  neissex  23460  cnpnei  23597  lmcnp  23637  ordthaus  23717  llynlly  23811  restnlly  23816  llyidm  23822  nllyidm  23823  ptbasin  23911  txcnp  23954  ist0-4  24063  kqt0lem  24070  isr0  24071  regr1lem2  24074  cmphmph  24122  connhmph  24123  fbun  24174  trfbas2  24177  isfil2  24190  isfild  24192  infil  24197  fbasfip  24202  fbasrn  24218  trfil2  24221  rnelfmlem  24286  fmfnfmlem3  24290  flimopn  24309  txflf  24340  fclsnei  24353  fclsfnflim  24361  fcfnei  24369  clssubg  24443  tgphaus  24451  qustgplem  24455  tsmsadd  24481  psmetxrge0  24647  psmetlecl  24649  xmetlecl  24680  xmettpos  24683  imasdsf1olem  24707  imasf1oxmet  24709  imasf1omet  24710  elbl3ps  24725  elbl3  24726  metss  24842  comet  24847  stdbdxmet  24849  stdbdmet  24850  methaus  24854  nrmmetd  24908  abvmet  24909  isngp4  24946  subgngp  24969  nmoi2  25064  nmoleub  25065  nmoid  25076  bl2ioo  25126  zcld  25148  divcn  25204  divccn  25209  cncfcdm  25234  divccncf  25242  icoopnst  25275  clmzlmvsca  25449  cph2ass  25549  tcphcph  25573  cfilfcls  25610  bcthlem2  25661  rrxmet  25744  rrxdstprj1  25745  rrxdsfi  25747  cldcss  25777  dvrec  26290  dvmptfsum  26310  aalioulem3  26676  taylply2  26710  efsubm  26894  dchrelbasd  27581  dchrmulcl  27591  2sqreulem3  27795  pntrmax  27906  padicabv  27972  nosupbnd2  28088  noinfbnd2  28103  sltsd  28169  divmulsw  28594  axtgcont  28946  xmstrkgc  29478  axsegconlem1  29510  axlowdimlem15  29549  usgredg2vlem1  29821  usgredg2vlem2  29822  iswlkon  30251  wwlksnextsurj  30504  elwwlks2  30573  elwspths2spth  30574  frrusgrord  30957  numclwwlk1lem2foalem  30967  grpoidinvlem2  31122  grpoidinvlem3  31123  ablo4  31167  ablomuldiv  31169  nvaddsub4  31274  nvmeq0  31275  sspmval  31350  sspimsval  31355  lnosub  31376  dipsubdir  31465  hvadd4  31653  hvpncan  31656  his35  31705  hiassdi  31708  shscli  31934  shmodsi  32006  chj4  32152  spansnmul  32181  spansncol  32185  spanunsni  32196  hoadd4  32401  hosubadd4  32431  lnopl  32531  unopf1o  32533  counop  32538  lnfnl  32548  hmopadj2  32558  eighmre  32580  lnopmi  32617  lnophsi  32618  hmops  32637  hmopm  32638  cnlnadjlem2  32685  adjmul  32709  adjadd  32710  kbass6  32738  mdslj1i  32936  mdslj2i  32937  mdslmd1lem1  32942  mdslmd2i  32947  chirredlem3  33009  isoun  33352  xdivmul  33547  odutos  33585  lmodvslmhm  33667  isarchi2  33802  archiabllem2  33814  imasmhm  33971  imasghm  33972  imasrhm  33973  imaslmhm  33974  quslmhm  33976  tngdim  34301  fedgmullem2  34318  metider  34582  pl1cn  34643  rossros  34869  ismeas  34888  dya2iocnei  34970  inelcarsg  34999  signstfvc  35259  bnj563  35430  fisshasheq  36017  cnpconn  36119  cvmseu  36165  elmrsubrn  36409  mrsubco  36410  fneint  37266  fnessref  37275  tailfb  37295  onsucuni3  38433  pibt2  38483  ptrecube  38681  poimirlem4  38685  heicant  38716  mblfinlem1  38718  mblfinlem2  38719  mblfinlem3  38720  mblfinlem4  38721  cnambfre  38729  itg2addnclem2  38733  ftc1anclem5  38758  ftc1anclem6  38759  metf1o  38832  isbnd3b  38862  equivbnd  38867  heiborlem3  38890  rrnmet  38906  rrndstprj1  38907  rrntotbnd  38913  exidcl  38953  ghomco  38968  ghomdiv  38969  grpokerinj  38970  rngoneglmul  39020  rngonegrmul  39021  rngosubdi  39022  rngosubdir  39023  isdrngo2  39035  rngohomco  39051  rngoisocnv  39058  riscer  39065  crngm4  39080  crngohomfo  39083  idlsubcl  39100  inidl  39107  keridl  39109  ispridlc  39147  pridlc3  39150  dmncan1  39153  lflvscl  40277  3dim0  40657  linepsubN  40952  cdlemg2fvlem  41794  trlcoat  41923  istendod  41962  dva1dim  42185  dvhvaddcomN  42296  dihf11  42467  dihlatat  42537  sn-sup2  43698  fsuppssind  43764  mhphf  43768  ismrc  43855  isnacs3  43864  mzpindd  43900  pellex  43985  monotoddzzfi  44092  lermxnn0  44100  rmyeq0  44103  rmyeq  44104  lermy  44105  jm2.27  44158  lsmfgcl  44219  fsumcnsrcl  44311  rngunsnply  44314  gsumws3  45339  mnringmulrcld  45369  nzin  45445  ofdivrec  45453  ofdivcan4  45454  chordthmALT  46057  wessf1ornlem  46342  projf1o  46353  ltdiv23neg  46547  fmulcl  46735  prproropf1olem2  48728  prproropf1olem4  48730  mgmplusgiopALT  49433  idomcanl  49586  itsclc0xyqsolb  50024  toslat  50238  cicerALT  50302