Theorem 3expb 1258

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3adant3r1  1266  3adant3r2  1267  3adant3r3  1268  3adant1l  1310  3adant1r  1311  mp3an1  1403  sotri  5442  fnfco  5982  mpt2eq3dva  6617  oprres  6700  fovrnda  6703  grprinvd  6771  fnmpt2ovd  7139  offval22  7140  bropfvvvvlem  7143  fnsuppres  7209  suppsssn  7217  sprmpt2d  7237  oaass  7528  omlimcl  7545  odi  7546  nnmsucr  7592  cflim2  8968  mulcanenq  9661  mul4  10084  add4  10135  2addsub  10174  addsubeq4  10175  subadd4  10204  muladd  10341  ltleadd  10390  divmul  10567  divne0  10576  div23  10583  div12  10586  divsubdir  10600  divcan5  10606  divmuleq  10609  divcan6  10611  divdiv32  10612  div2sub  10729  letrp1  10744  lemul12b  10759  lediv1  10767  lt2mul2div  10780  lemuldiv  10782  ltdiv2  10788  ledivdiv  10791  lediv2  10792  ltdiv23  10793  lediv23  10794  sup2  10858  cju  10893  nndivre  10933  nndivtr  10939  nn0addge1  11216  nn0addge2  11217  peano2uz2  11341  uzind  11345  uzind3  11347  fzind  11351  fnn0ind  11352  uzind4  11622  qre  11669  irrmul  11689  rpdivcl  11732  rerpdivcl  11737  xrinfmsslem  12010  ixxin  12063  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzaddel  12246  fzadd2  12247  fzrev  12273  modlt  12541  modcyc  12567  axdc4uzlem  12644  expdiv  12773  swrd00  13270  swrdcl  13271  swrd0  13286  swrdccat  13344  swrdco  13434  2shfti  13668  isermulc2  14236  fsummulc2  14358  dvdscmulr  14848  dvdsmulcr  14849  dvds2add  14853  dvds2sub  14854  dvdstr  14856  alzdvds  14880  divalg2  14966  dvdslegcd  15064  lcmgcdlem  15157  lcmgcdeq  15163  isprm6  15264  pcqcl  15399  vdwmc2  15521  ressinbas  15763  cicer  16289  isposd  16778  pleval2i  16787  tosso  16859  poslubmo  16969  posglbmo  16970  mgmplusf  17074  ismndd  17136  imasmnd2  17150  idmhm  17167  issubm2  17171  0mhm  17181  resmhm  17182  resmhm2  17183  resmhm2b  17184  mhmco  17185  mhmima  17186  submacs  17188  prdspjmhm  17190  pwsdiagmhm  17192  pwsco1mhm  17193  pwsco2mhm  17194  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  grpinvcnv  17306  grpinvnzcl  17310  grpsubf  17317  imasgrp2  17353  qusgrp2  17356  mhmfmhm  17361  mulgnnsubcl  17376  mulgnndir  17392  mulgnndirOLD  17393  issubg4  17436  isnsg3  17451  nsgacs  17453  nsgid  17463  qusadd  17474  ghmmhm  17493  ghmmhmb  17494  idghm  17498  resghm  17499  ghmf1  17512  qusghm  17520  gaid  17555  subgga  17556  gasubg  17558  invoppggim  17613  gsmsymgrfix  17671  lsmidm  17900  pj1ghm  17939  mulgnn0di  18054  mulgmhm  18056  mulgghm  18057  ghmfghm  18059  invghm  18062  ghmplusg  18072  ablnsg  18073  qusabl  18091  gsumval3eu  18128  gsumval3  18131  gsumzcl2  18134  gsumzaddlem  18144  gsumzadd  18145  gsumzmhm  18160  gsumzoppg  18167  srgfcl  18338  srgmulgass  18354  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  issubrg2  18623  issrngd  18684  islmodd  18692  lmodscaf  18708  lcomf  18725  lmodvsghm  18747  lssacs  18788  idlmhm  18862  invlmhm  18863  lmhmvsca  18866  reslmhm2  18874  reslmhm2b  18875  pwsdiaglmhm  18878  pwssplit2  18881  pwssplit3  18882  issubrngd2  19010  qusrhm  19058  crngridl  19059  quscrng  19061  isnzr2  19084  domnmuln0  19119  opprdomn  19122  asclghm  19159  asclrhm  19163  psraddcl  19204  psrvscacl  19214  psrass23  19231  psrbagev1  19331  coe1sclmulfv  19474  cply1mul  19485  expmhm  19634  zntoslem  19724  znfld  19728  psgnghm  19745  phlipf  19816  frlmup1  19956  mndvcl  20016  matbas2d  20048  submaeval  20207  minmar1eval  20274  cpmatacl  20340  pmatcollpw1  20400  pmatcollpw  20405  tgclb  20585  topbas  20587  ntrss  20669  mretopd  20706  neissex  20741  cnpnei  20878  lmcnp  20918  ordthaus  20998  llynlly  21090  restnlly  21095  llyidm  21101  nllyidm  21102  ptbasin  21190  txcnp  21233  ist0-4  21342  kqt0lem  21349  isr0  21350  regr1lem2  21353  cmphmph  21401  conhmph  21402  fbun  21454  trfbas2  21457  isfil2  21470  isfild  21472  infil  21477  fbasfip  21482  fbasrn  21498  trfil2  21501  rnelfmlem  21566  fmfnfmlem3  21570  flimopn  21589  txflf  21620  fclsnei  21633  fclsfnflim  21641  fcfnei  21649  clssubg  21722  tgphaus  21730  qustgplem  21734  tsmsadd  21760  psmetxrge0  21928  psmetlecl  21930  xmetlecl  21961  xmettpos  21964  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  elbl3ps  22006  elbl3  22007  metss  22123  comet  22128  stdbdxmet  22130  stdbdmet  22131  methaus  22135  nrmmetd  22189  abvmet  22190  isngp4  22226  subgngp  22249  nmoi2  22344  nmoleub  22345  nmoid  22356  bl2ioo  22403  zcld  22424  divcn  22479  divccn  22484  cncffvrn  22509  divccncf  22517  icoopnst  22546  clmzlmvsca  22721  cph2ass  22821  tchcph  22844  cfilfcls  22880  bcthlem2  22930  rrxmet  22999  rrxdstprj1  23000  cldcss  23020  dvrec  23524  dvmptfsum  23542  aalioulem3  23893  taylply2  23926  efsubm  24101  dchrelbasd  24764  dchrmulcl  24774  pntrmax  25053  padicabv  25119  axtgcont  25168  xmstrkgc  25566  axsegconlem1  25597  axlowdimlem15  25636  usgraidx2vlem1  25920  usgraidx2vlem2  25921  wlknwwlkninj  26239  wwlkextsur  26259  3cyclfrgrarn  26540  frgrawopreg  26576  grpoidinvlem2  26743  grpoidinvlem3  26744  ablo4  26788  ablomuldiv  26790  nvaddsub4  26896  nvmeq0  26897  sspmval  26972  sspimsval  26977  lnosub  26998  dipsubdir  27087  sspph  27094  hvadd4  27277  hvpncan  27280  his35  27329  hiassdi  27332  shscli  27560  shmodsi  27632  chj4  27778  spansnmul  27807  spansncol  27811  spanunsni  27822  hoadd4  28027  hosubadd4  28057  lnopl  28157  unopf1o  28159  counop  28164  lnfnl  28174  hmopadj2  28184  eighmre  28206  lnopmi  28243  lnophsi  28244  hmops  28263  hmopm  28264  cnlnadjlem2  28311  adjmul  28335  adjadd  28336  kbass6  28364  mdslj1i  28562  mdslj2i  28563  mdslmd1lem1  28568  mdslmd2i  28573  chirredlem3  28635  isoun  28862  xdivmul  28964  odutos  28994  isarchi2  29070  archiabllem2  29082  metider  29265  pl1cn  29329  rossros  29570  ismeas  29589  dya2iocnei  29671  inelcarsg  29700  bnj563  30067  cnpcon  30466  cvmseu  30512  elmrsubrn  30671  mrsubco  30672  subdivcomb1  30864  fneint  31513  fnessref  31522  tailfb  31542  onsucuni3  32391  ptrecube  32579  poimirlem4  32583  heicant  32614  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  cnambfre  32628  itg2addnclem2  32632  ftc1anclem5  32659  ftc1anclem6  32660  metf1o  32721  isbnd3b  32754  equivbnd  32759  heiborlem3  32782  rrnmet  32798  rrndstprj1  32799  rrntotbnd  32805  exidcl  32845  ghomco  32860  ghomdiv  32861  grpokerinj  32862  rngoneglmul  32912  rngonegrmul  32913  rngosubdi  32914  rngosubdir  32915  isdrngo2  32927  rngohomco  32943  rngoisocnv  32950  riscer  32957  crngm4  32972  crngohomfo  32975  idlsubcl  32992  inidl  32999  keridl  33001  ispridlc  33039  pridlc3  33042  dmncan1  33045  lflvscl  33382  3dim0  33761  linepsubN  34056  cdlemg2fvlem  34900  trlcoat  35029  istendod  35068  dva1dim  35291  dvhvaddcomN  35403  dihf11  35574  dihlatat  35644  ismrc  36282  isnacs3  36291  mzpindd  36327  pellex  36417  monotoddzzfi  36525  lermxnn0  36535  rmyeq0  36538  rmyeq  36539  lermy  36540  jm2.27  36593  lsmfgcl  36662  fsumcnsrcl  36755  rngunsnply  36762  isdomn3  36801  gsumws3  37521  nzin  37539  ofdivrec  37547  ofdivcan4  37548  chordthmALT  38191  projf1o  38381  ltdiv23neg  38558  fmulcl  38648  rrxdsfi  39181  usgredg2vlem1  40452  usgredg2vlem2  40453  upgrwlkedg  40850  iswlkOn  40865  upgr2wlk  40876  wlknwwlksninj  41086  wwlksnextsur  41106  elwwlks2  41170  elwspths2spth  41171  upgreupthi  41376  frgrwopreg  41486  frgr2wwlk1  41494  ismgmd  41566  idmgmhm  41578  resmgmhm  41588  resmgmhm2  41589  resmgmhm2b  41590  mgmhmco  41591  mgmhmima  41592  submgmacs  41594  mgmplusgiopALT  41620  c0mgm  41699  c0mhm  41700