Theorem 3expb 1113

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3expia  1114  3adant3r1  1175  3adant3r2  1176  3adant3r3  1177  mp3an1  1440  sotri  5870  fnfco  6418  mpoeq3dva  7096  oprres  7179  fovrnda  7182  grprinvd  7250  fnmpoovd  7645  offval22  7646  bropfvvvvlem  7649  fnsuppres  7715  suppsssn  7723  sprmpod  7748  oaass  8044  omlimcl  8061  odi  8062  nnmsucr  8108  cflim2  9538  mulcanenq  10235  mul4  10661  add4  10713  2addsub  10754  addsubeq4  10755  subadd4  10784  muladd  10926  ltleadd  10977  divmul  11155  divne0  11164  div23  11171  div12  11174  divsubdir  11188  subdivcomb1  11189  divcan5  11196  divmuleq  11199  divcan6  11201  divdiv32  11202  div2sub  11319  letrp1  11338  lemul12b  11351  lediv1  11359  lt2mul2div  11372  lemuldiv  11374  ltdiv2  11380  ledivdiv  11383  lediv2  11384  ltdiv23  11385  lediv23  11386  sup2  11451  cju  11488  nndivre  11532  nndivtr  11538  nn0addge1  11797  nn0addge2  11798  peano2uz2  11924  uzind  11928  uzind3  11930  fzind  11934  fnn0ind  11935  uzind4  12159  qre  12206  irrmul  12227  rpdivcl  12268  rerpdivcl  12273  xrinfmsslem  12555  ixxin  12609  iccshftr  12726  iccshftl  12728  iccdil  12730  icccntr  12732  fzaddel  12795  fzadd2  12796  fzrev  12824  modlt  13102  modcyc  13128  axdc4uzlem  13205  expdiv  13334  fundmge2nop0  13700  swrd00  13846  swrdcl  13847  swrdnnn0nd  13858  swrd0  13860  swrdwrdsymb  13864  swrdccat  13937  splid  13955  swrdco  14039  2shfti  14277  isermulc2  14852  fsummulc2  14976  dvdscmulr  15475  dvdsmulcr  15476  dvds2add  15480  dvds2sub  15481  dvdstr  15483  alzdvds  15507  divalg2  15593  dvdslegcd  15690  lcmgcdlem  15783  lcmgcdeq  15789  isprm6  15891  pcqcl  16026  vdwmc2  16148  ressinbas  16393  cicer  16909  isposd  17398  pleval2i  17407  tosso  17479  poslubmo  17589  posglbmo  17590  mgmplusf  17694  ismndd  17756  imasmnd2  17770  idmhm  17787  issubm2  17791  0mhm  17801  resmhm  17802  resmhm2  17803  resmhm2b  17804  mhmco  17805  mhmima  17806  submacs  17808  prdspjmhm  17810  pwsdiagmhm  17812  pwsco1mhm  17813  pwsco2mhm  17814  gsumwsubmcl  17818  gsumccat  17821  gsumwmhm  17825  grpinvcnv  17928  grpinvnzcl  17932  grpsubf  17939  imasgrp2  17975  qusgrp2  17978  mhmfmhm  17983  mulgnnsubcl  17999  mulgnndir  18014  issubg4  18056  isnsg3  18071  nsgacs  18073  nsgid  18083  qusadd  18094  ghmmhm  18113  ghmmhmb  18114  idghm  18118  resghm  18119  ghmf1  18132  qusghm  18140  gaid  18174  subgga  18175  gasubg  18177  invoppggim  18233  gsmsymgrfix  18291  lsmidm  18521  pj1ghm  18560  mulgnn0di  18675  mulgmhm  18677  mulgghm  18678  ghmfghm  18680  invghm  18683  ghmplusg  18693  ablnsg  18694  qusabl  18712  gsumval3eu  18749  gsumval3  18752  gsumzcl2  18755  gsumzaddlem  18765  gsumzadd  18766  gsumzmhm  18781  gsumzoppg  18788  srgfcl  18959  srgmulgass  18975  srglmhm  18979  srgrmhm  18980  ringlghm  19048  ringrghm  19049  issubrg2  19249  issrngd  19326  islmodd  19334  lmodscaf  19350  lcomf  19367  lmodvsghm  19389  rmodislmodlem  19395  lssacs  19433  idlmhm  19507  invlmhm  19508  lmhmvsca  19511  reslmhm2  19519  reslmhm2b  19520  pwsdiaglmhm  19523  pwssplit2  19526  pwssplit3  19527  issubrngd2  19655  qusrhm  19703  crngridl  19704  quscrng  19706  isnzr2  19729  domnmuln0  19764  opprdomn  19767  asclghm  19804  asclrhm  19811  rnasclmulcl  19814  psraddcl  19855  psrvscacl  19865  psrass23  19882  psrbagev1  19981  coe1sclmulfv  20138  cply1mul  20149  expmhm  20300  zntoslem  20389  znfld  20393  psgnghm  20410  phlipf  20482  frlmup1  20628  mndvcl  20688  matbas2d  20720  submaeval  20879  minmar1eval  20946  cpmatacl  21012  pmatcollpw1  21072  pmatcollpw  21077  tgclb  21266  topbas  21268  ntrss  21351  mretopd  21388  neissex  21423  cnpnei  21560  lmcnp  21600  ordthaus  21680  llynlly  21773  restnlly  21778  llyidm  21784  nllyidm  21785  ptbasin  21873  txcnp  21916  ist0-4  22025  kqt0lem  22032  isr0  22033  regr1lem2  22036  cmphmph  22084  connhmph  22085  fbun  22136  trfbas2  22139  isfil2  22152  isfild  22154  infil  22159  fbasfip  22164  fbasrn  22180  trfil2  22183  rnelfmlem  22248  fmfnfmlem3  22252  flimopn  22271  txflf  22302  fclsnei  22315  fclsfnflim  22323  fcfnei  22331  clssubg  22404  tgphaus  22412  qustgplem  22416  tsmsadd  22442  psmetxrge0  22610  psmetlecl  22612  xmetlecl  22643  xmettpos  22646  imasdsf1olem  22670  imasf1oxmet  22672  imasf1omet  22673  elbl3ps  22688  elbl3  22689  metss  22805  comet  22810  stdbdxmet  22812  stdbdmet  22813  methaus  22817  nrmmetd  22871  abvmet  22872  isngp4  22908  subgngp  22931  nmoi2  23026  nmoleub  23027  nmoid  23038  bl2ioo  23087  zcld  23108  divcn  23163  divccn  23168  cncffvrn  23193  divccncf  23201  icoopnst  23230  clmzlmvsca  23404  cph2ass  23504  tcphcph  23527  cfilfcls  23564  bcthlem2  23615  rrxmet  23698  rrxdstprj1  23699  rrxdsfi  23701  cldcss  23731  dvrec  24239  dvmptfsum  24259  aalioulem3  24610  taylply2  24643  efsubm  24820  dchrelbasd  25501  dchrmulcl  25511  2sqreulem3  25715  pntrmax  25826  padicabv  25892  axtgcont  25941  xmstrkgc  26359  axsegconlem1  26390  axlowdimlem15  26429  usgredg2vlem1  26694  usgredg2vlem2  26695  iswlkon  27125  wwlksnextsurj  27364  elwwlks2  27431  elwspths2spth  27432  frrusgrord  27808  numclwwlk1lem2foalem  27818  grpoidinvlem2  27969  grpoidinvlem3  27970  ablo4  28014  ablomuldiv  28016  nvaddsub4  28121  nvmeq0  28122  sspmval  28197  sspimsval  28202  lnosub  28223  dipsubdir  28312  hvadd4  28500  hvpncan  28503  his35  28552  hiassdi  28555  shscli  28781  shmodsi  28853  chj4  28999  spansnmul  29028  spansncol  29032  spanunsni  29043  hoadd4  29248  hosubadd4  29278  lnopl  29378  unopf1o  29380  counop  29385  lnfnl  29395  hmopadj2  29405  eighmre  29427  lnopmi  29464  lnophsi  29465  hmops  29484  hmopm  29485  cnlnadjlem2  29532  adjmul  29556  adjadd  29557  kbass6  29585  mdslj1i  29783  mdslj2i  29784  mdslmd1lem1  29789  mdslmd2i  29794  chirredlem3  29856  isoun  30121  xdivmul  30281  odutos  30320  isarchi2  30448  archiabllem2  30460  lmodvslmhm  30495  quslmhm  30574  tngdim  30611  fedgmullem2  30626  metider  30747  pl1cn  30811  rossros  31052  ismeas  31071  dya2iocnei  31153  inelcarsg  31182  bnj563  31627  fisshasheq  31962  cnpconn  32087  cvmseu  32133  elmrsubrn  32377  mrsubco  32378  nosupbnd2  32827  fneint  33307  fnessref  33316  tailfb  33336  onsucuni3  34200  pibt2  34250  ptrecube  34444  poimirlem4  34448  heicant  34479  mblfinlem1  34481  mblfinlem2  34482  mblfinlem3  34483  mblfinlem4  34484  cnambfre  34492  itg2addnclem2  34496  ftc1anclem5  34523  ftc1anclem6  34524  metf1o  34583  isbnd3b  34616  equivbnd  34621  heiborlem3  34644  rrnmet  34660  rrndstprj1  34661  rrntotbnd  34667  exidcl  34707  ghomco  34722  ghomdiv  34723  grpokerinj  34724  rngoneglmul  34774  rngonegrmul  34775  rngosubdi  34776  rngosubdir  34777  isdrngo2  34789  rngohomco  34805  rngoisocnv  34812  riscer  34819  crngm4  34834  crngohomfo  34837  idlsubcl  34854  inidl  34861  keridl  34863  ispridlc  34901  pridlc3  34904  dmncan1  34907  lflvscl  35765  3dim0  36145  linepsubN  36440  cdlemg2fvlem  37282  trlcoat  37411  istendod  37450  dva1dim  37673  dvhvaddcomN  37784  dihf11  37955  dihlatat  38025  ismrc  38804  isnacs3  38813  mzpindd  38849  pellex  38938  monotoddzzfi  39045  lermxnn0  39053  rmyeq0  39056  rmyeq  39057  lermy  39058  jm2.27  39111  lsmfgcl  39180  fsumcnsrcl  39272  rngunsnply  39279  isdomn3  39310  gsumws3  40056  nzin  40209  ofdivrec  40217  ofdivcan4  40218  chordthmALT  40827  wessf1ornlem  41006  projf1o  41020  ltdiv23neg  41228  fmulcl  41425  prproropf1olem2  43170  prproropf1olem4  43172  ismgmd  43547  idmgmhm  43559  resmgmhm  43569  resmgmhm2  43570  resmgmhm2b  43571  mgmhmco  43572  mgmhmima  43573  submgmacs  43575  mgmplusgiopALT  43601  c0mgm  43680  c0mhm  43681  itsclc0xyqsolb  44260