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 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  1122  3adant3r1  1184  3adant3r2  1185  3adant3r3  1186  mp3an1  1451  sotri  6090  fnfco  6705  mpoeq3dva  7444  oprres  7535  fovcdmda  7538  fnmpoovd  8037  offval22  8038  bropfvvvvlem  8041  fnsuppres  8141  suppsssn  8151  sprmpod  8174  oaass  8496  omlimcl  8513  odi  8514  nnmsucr  8561  nnasmo  8599  unfi  9105  ttrclse  9648  cflim2  10185  mulcanenq  10883  mul4  11314  add4  11367  2addsub  11407  addsubeq4  11408  subadd4  11438  muladd  11582  ltleadd  11633  divmul  11812  divne0  11821  div23  11828  div12  11831  div11  11837  divsubdir  11848  subdivcomb1  11850  divcan5  11857  divmuleq  11860  divcan6  11862  divdiv32  11863  div2sub  11980  letrp1  11999  lemul12b  12012  lediv1  12021  lt2mul2div  12034  lemuldiv  12036  ltdiv2  12042  ledivdiv  12045  lediv2  12046  ltdiv23  12047  lediv23  12048  sup2  12112  cju  12155  nndivre  12218  nndivtr  12224  nn0addge1  12483  nn0addge2  12484  peano2uz2  12617  uzind  12621  uzind3  12623  fzind  12627  fnn0ind  12628  uzind4  12856  qre  12903  irrmul  12924  rpdivcl  12969  rerpdivcl  12974  xrinfmsslem  13260  ixxin  13315  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzaddel  13512  fzadd2  13513  fzrev  13541  modlt  13839  modcyc  13865  axdc4uzlem  13945  expdiv  14075  fundmge2nop0  14464  swrd00  14607  swrdcl  14608  swrdnnn0nd  14619  swrd0  14621  swrdwrdsymb  14625  ccatpfx  14663  swrdccat  14697  splid  14715  swrdco  14799  2shfti  15042  isermulc2  15620  fsummulc2  15746  dvdscmulr  16253  dvdsmulcr  16254  dvds2add  16259  dvds2sub  16260  dvdstr  16263  alzdvds  16289  divalg2  16374  dvdslegcd  16473  lcmgcdlem  16575  lcmgcdeq  16581  isprm6  16684  pcqcl  16827  vdwmc2  16950  ressinbas  17215  cicer  17773  isposd  18288  pleval2i  18300  poslubmo  18375  posglbmo  18376  tosso  18383  mgmplusf  18618  ismgmd  18620  grpinva  18642  idmgmhm  18669  resmgmhm  18679  resmgmhm2  18680  resmgmhm2b  18681  mgmhmco  18682  mgmhmima  18683  submgmacs  18685  sgrpidmnd  18707  ismndd  18724  imasmnd2  18742  idmhm  18763  mndvcl  18765  issubm2  18772  0mhm  18787  resmhm  18788  resmhm2  18789  resmhm2b  18790  mhmco  18791  mhmimalem  18792  submacs  18795  prdspjmhm  18797  pwsdiagmhm  18799  pwsco1mhm  18800  pwsco2mhm  18801  gsumwsubmcl  18805  gsumsgrpccat  18808  gsumwmhm  18813  grpinvcnv  18982  grpinvnzcl  18987  grpsubf  18995  imasgrp2  19031  qusgrp2  19034  mhmfmhm  19041  mulgnnsubcl  19062  mulgnndir  19079  issubg4  19121  isnsg3  19135  nsgacs  19137  nsgid  19145  qusadd  19163  qus0subgadd  19174  ghmmhm  19201  ghmmhmb  19202  idghm  19206  resghm  19207  ghmf1  19221  qusghm  19230  gaid  19274  subgga  19275  gasubg  19277  invoppggim  19335  gsmsymgrfix  19403  smndlsmidm  19631  pj1ghm  19678  mulgnn0di  19800  mulgmhm  19802  mulgghm  19803  ghmfghm  19805  invghm  19808  ghmplusg  19821  ablnsg  19822  qusabl  19840  gsumval3eu  19879  gsumval3  19882  gsumzcl2  19885  gsumzaddlem  19896  gsumzadd  19897  gsumzmhm  19912  gsumzoppg  19919  srgfcl  20177  srgcom4lem  20194  srgmulgass  20198  srglmhm  20202  srgrmhm  20203  ringcomlem  20260  ringlghm  20293  ringrghm  20294  pwspjmhmmgpd  20307  c0mgm  20439  c0mhm  20440  isnzr2  20495  subrngringnsg  20530  issubrng2  20535  rhmimasubrnglem  20542  issubrg2  20569  domnmuln0  20686  isdomn3  20692  issrngd  20832  islmodd  20861  lmodscaf  20879  lcomf  20896  lmodvsghm  20918  rmodislmodlem  20924  lssacs  20962  idlmhm  21036  invlmhm  21037  lmhmvsca  21040  reslmhm2  21048  reslmhm2b  21049  pwsdiaglmhm  21052  pwssplit2  21055  pwssplit3  21056  issubrgd  21184  qusrhm  21274  qusmul2idl  21277  crngridl  21278  qusmulrng  21280  expmhm  21416  zntoslem  21536  znfld  21540  psgnghm  21560  phlipf  21632  frlmup1  21778  asclghm  21862  asclrhm  21870  rnasclmulcl  21874  psraddcl  21918  psrvscacl  21930  psrass23  21947  psrbagev1  22055  coe1sclmulfv  22248  cply1mul  22261  evls1fpws  22334  rhmply1vsca  22353  matbas2d  22388  submaeval  22547  minmar1eval  22614  cpmatacl  22681  pmatcollpw1  22741  pmatcollpw  22746  tgclb  22935  topbas  22937  ntrss  23020  mretopd  23057  neissex  23092  cnpnei  23229  lmcnp  23269  ordthaus  23349  llynlly  23442  restnlly  23447  llyidm  23453  nllyidm  23454  ptbasin  23542  txcnp  23585  ist0-4  23694  kqt0lem  23701  isr0  23702  regr1lem2  23705  cmphmph  23753  connhmph  23754  fbun  23805  trfbas2  23808  isfil2  23821  isfild  23823  infil  23828  fbasfip  23833  fbasrn  23849  trfil2  23852  rnelfmlem  23917  fmfnfmlem3  23921  flimopn  23940  txflf  23971  fclsnei  23984  fclsfnflim  23992  fcfnei  24000  clssubg  24074  tgphaus  24082  qustgplem  24086  tsmsadd  24112  psmetxrge0  24278  psmetlecl  24280  xmetlecl  24311  xmettpos  24314  imasdsf1olem  24338  imasf1oxmet  24340  imasf1omet  24341  elbl3ps  24356  elbl3  24357  metss  24473  comet  24478  stdbdxmet  24480  stdbdmet  24481  methaus  24485  nrmmetd  24539  abvmet  24540  isngp4  24577  subgngp  24600  nmoi2  24695  nmoleub  24696  nmoid  24707  bl2ioo  24757  zcld  24779  divcn  24835  divccn  24840  cncfcdm  24865  divccncf  24873  icoopnst  24906  clmzlmvsca  25080  cph2ass  25180  tcphcph  25204  cfilfcls  25241  bcthlem2  25292  rrxmet  25375  rrxdstprj1  25376  rrxdsfi  25378  cldcss  25408  dvrec  25922  dvmptfsum  25942  aalioulem3  26300  taylply2  26333  efsubm  26515  dchrelbasd  27202  dchrmulcl  27212  2sqreulem3  27416  pntrmax  27527  padicabv  27593  nosupbnd2  27680  noinfbnd2  27695  sltsd  27760  divmulsw  28185  axtgcont  28537  xmstrkgc  28954  axsegconlem1  28986  axlowdimlem15  29025  usgredg2vlem1  29294  usgredg2vlem2  29295  iswlkon  29724  wwlksnextsurj  29968  elwwlks2  30037  elwspths2spth  30038  frrusgrord  30411  numclwwlk1lem2foalem  30421  grpoidinvlem2  30576  grpoidinvlem3  30577  ablo4  30621  ablomuldiv  30623  nvaddsub4  30728  nvmeq0  30729  sspmval  30804  sspimsval  30809  lnosub  30830  dipsubdir  30919  hvadd4  31107  hvpncan  31110  his35  31159  hiassdi  31162  shscli  31388  shmodsi  31460  chj4  31606  spansnmul  31635  spansncol  31639  spanunsni  31650  hoadd4  31855  hosubadd4  31885  lnopl  31985  unopf1o  31987  counop  31992  lnfnl  32002  hmopadj2  32012  eighmre  32034  lnopmi  32071  lnophsi  32072  hmops  32091  hmopm  32092  cnlnadjlem2  32139  adjmul  32163  adjadd  32164  kbass6  32192  mdslj1i  32390  mdslj2i  32391  mdslmd1lem1  32396  mdslmd2i  32401  chirredlem3  32463  isoun  32775  xdivmul  32984  odutos  33028  lmodvslmhm  33111  isarchi2  33246  archiabllem2  33258  imasmhm  33414  imasghm  33415  imasrhm  33416  imaslmhm  33417  quslmhm  33419  tngdim  33757  fedgmullem2  33774  metider  34038  pl1cn  34099  rossros  34324  ismeas  34343  dya2iocnei  34426  inelcarsg  34455  signstfvc  34718  bnj563  34886  fisshasheq  35297  cnpconn  35412  cvmseu  35458  elmrsubrn  35702  mrsubco  35703  fneint  36530  fnessref  36539  tailfb  36559  onsucuni3  37683  pibt2  37733  ptrecube  37941  poimirlem4  37945  heicant  37976  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  cnambfre  37989  itg2addnclem2  37993  ftc1anclem5  38018  ftc1anclem6  38019  metf1o  38076  isbnd3b  38106  equivbnd  38111  heiborlem3  38134  rrnmet  38150  rrndstprj1  38151  rrntotbnd  38157  exidcl  38197  ghomco  38212  ghomdiv  38213  grpokerinj  38214  rngoneglmul  38264  rngonegrmul  38265  rngosubdi  38266  rngosubdir  38267  isdrngo2  38279  rngohomco  38295  rngoisocnv  38302  riscer  38309  crngm4  38324  crngohomfo  38327  idlsubcl  38344  inidl  38351  keridl  38353  ispridlc  38391  pridlc3  38394  dmncan1  38397  lflvscl  39523  3dim0  39903  linepsubN  40198  cdlemg2fvlem  41040  trlcoat  41169  istendod  41208  dva1dim  41431  dvhvaddcomN  41542  dihf11  41713  dihlatat  41783  sn-sup2  42936  fsuppssind  43026  mhphf  43030  ismrc  43133  isnacs3  43142  mzpindd  43178  pellex  43263  monotoddzzfi  43370  lermxnn0  43378  rmyeq0  43381  rmyeq  43382  lermy  43383  jm2.27  43436  lsmfgcl  43502  fsumcnsrcl  43594  rngunsnply  43597  gsumws3  44623  mnringmulrcld  44655  nzin  44745  ofdivrec  44753  ofdivcan4  44754  chordthmALT  45359  wessf1ornlem  45615  projf1o  45626  ltdiv23neg  45823  fmulcl  46011  prproropf1olem2  47964  prproropf1olem4  47966  mgmplusgiopALT  48670  itsclc0xyqsolb  49246  toslat  49457  cicerALT  49521