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  6082  fnfco  6697  mpoeq3dva  7433  oprres  7524  fovcdmda  7527  fnmpoovd  8027  offval22  8028  bropfvvvvlem  8031  fnsuppres  8131  suppsssn  8141  sprmpod  8164  oaass  8486  omlimcl  8503  odi  8504  nnmsucr  8551  nnasmo  8589  unfi  9093  ttrclse  9634  cflim2  10171  mulcanenq  10869  mul4  11299  add4  11352  2addsub  11392  addsubeq4  11393  subadd4  11423  muladd  11567  ltleadd  11618  divmul  11797  divne0  11806  div23  11813  div12  11816  div11  11822  divsubdir  11833  subdivcomb1  11834  divcan5  11841  divmuleq  11844  divcan6  11846  divdiv32  11847  div2sub  11964  letrp1  11983  lemul12b  11996  lediv1  12005  lt2mul2div  12018  lemuldiv  12020  ltdiv2  12026  ledivdiv  12029  lediv2  12030  ltdiv23  12031  lediv23  12032  sup2  12096  cju  12139  nndivre  12184  nndivtr  12190  nn0addge1  12445  nn0addge2  12446  peano2uz2  12578  uzind  12582  uzind3  12584  fzind  12588  fnn0ind  12589  uzind4  12817  qre  12864  irrmul  12885  rpdivcl  12930  rerpdivcl  12935  xrinfmsslem  13221  ixxin  13276  iccshftr  13400  iccshftl  13402  iccdil  13404  icccntr  13406  fzaddel  13472  fzadd2  13473  fzrev  13501  modlt  13798  modcyc  13824  axdc4uzlem  13904  expdiv  14034  fundmge2nop0  14423  swrd00  14566  swrdcl  14567  swrdnnn0nd  14578  swrd0  14580  swrdwrdsymb  14584  ccatpfx  14622  swrdccat  14656  splid  14674  swrdco  14758  2shfti  15001  isermulc2  15579  fsummulc2  15705  dvdscmulr  16209  dvdsmulcr  16210  dvds2add  16215  dvds2sub  16216  dvdstr  16219  alzdvds  16245  divalg2  16330  dvdslegcd  16429  lcmgcdlem  16531  lcmgcdeq  16537  isprm6  16639  pcqcl  16782  vdwmc2  16905  ressinbas  17170  cicer  17728  isposd  18243  pleval2i  18255  poslubmo  18330  posglbmo  18331  tosso  18338  mgmplusf  18573  ismgmd  18575  grpinva  18597  idmgmhm  18624  resmgmhm  18634  resmgmhm2  18635  resmgmhm2b  18636  mgmhmco  18637  mgmhmima  18638  submgmacs  18640  sgrpidmnd  18662  ismndd  18679  imasmnd2  18697  idmhm  18718  mndvcl  18720  issubm2  18727  0mhm  18742  resmhm  18743  resmhm2  18744  resmhm2b  18745  mhmco  18746  mhmimalem  18747  submacs  18750  prdspjmhm  18752  pwsdiagmhm  18754  pwsco1mhm  18755  pwsco2mhm  18756  gsumwsubmcl  18760  gsumsgrpccat  18763  gsumwmhm  18768  grpinvcnv  18934  grpinvnzcl  18939  grpsubf  18947  imasgrp2  18983  qusgrp2  18986  mhmfmhm  18993  mulgnnsubcl  19014  mulgnndir  19031  issubg4  19073  isnsg3  19087  nsgacs  19089  nsgid  19097  qusadd  19115  qus0subgadd  19126  ghmmhm  19153  ghmmhmb  19154  idghm  19158  resghm  19159  ghmf1  19173  qusghm  19182  gaid  19226  subgga  19227  gasubg  19229  invoppggim  19287  gsmsymgrfix  19355  smndlsmidm  19583  pj1ghm  19630  mulgnn0di  19752  mulgmhm  19754  mulgghm  19755  ghmfghm  19757  invghm  19760  ghmplusg  19773  ablnsg  19774  qusabl  19792  gsumval3eu  19831  gsumval3  19834  gsumzcl2  19837  gsumzaddlem  19848  gsumzadd  19849  gsumzmhm  19864  gsumzoppg  19871  srgfcl  20129  srgcom4lem  20146  srgmulgass  20150  srglmhm  20154  srgrmhm  20155  ringcomlem  20212  ringlghm  20245  ringrghm  20246  pwspjmhmmgpd  20261  c0mgm  20393  c0mhm  20394  isnzr2  20449  subrngringnsg  20484  issubrng2  20489  rhmimasubrnglem  20496  issubrg2  20523  domnmuln0  20640  isdomn3  20646  issrngd  20786  islmodd  20815  lmodscaf  20833  lcomf  20850  lmodvsghm  20872  rmodislmodlem  20878  lssacs  20916  idlmhm  20991  invlmhm  20992  lmhmvsca  20995  reslmhm2  21003  reslmhm2b  21004  pwsdiaglmhm  21007  pwssplit2  21010  pwssplit3  21011  issubrgd  21139  qusrhm  21229  qusmul2idl  21232  crngridl  21233  qusmulrng  21235  expmhm  21389  zntoslem  21509  znfld  21513  psgnghm  21533  phlipf  21605  frlmup1  21751  asclghm  21836  asclrhm  21844  rnasclmulcl  21848  psraddcl  21892  psraddclOLD  21893  psrvscacl  21905  psrass23  21922  psrbagev1  22030  coe1sclmulfv  22223  cply1mul  22238  evls1fpws  22311  rhmply1vsca  22330  matbas2d  22365  submaeval  22524  minmar1eval  22591  cpmatacl  22658  pmatcollpw1  22718  pmatcollpw  22723  tgclb  22912  topbas  22914  ntrss  22997  mretopd  23034  neissex  23069  cnpnei  23206  lmcnp  23246  ordthaus  23326  llynlly  23419  restnlly  23424  llyidm  23430  nllyidm  23431  ptbasin  23519  txcnp  23562  ist0-4  23671  kqt0lem  23678  isr0  23679  regr1lem2  23682  cmphmph  23730  connhmph  23731  fbun  23782  trfbas2  23785  isfil2  23798  isfild  23800  infil  23805  fbasfip  23810  fbasrn  23826  trfil2  23829  rnelfmlem  23894  fmfnfmlem3  23898  flimopn  23917  txflf  23948  fclsnei  23961  fclsfnflim  23969  fcfnei  23977  clssubg  24051  tgphaus  24059  qustgplem  24063  tsmsadd  24089  psmetxrge0  24255  psmetlecl  24257  xmetlecl  24288  xmettpos  24291  imasdsf1olem  24315  imasf1oxmet  24317  imasf1omet  24318  elbl3ps  24333  elbl3  24334  metss  24450  comet  24455  stdbdxmet  24457  stdbdmet  24458  methaus  24462  nrmmetd  24516  abvmet  24517  isngp4  24554  subgngp  24577  nmoi2  24672  nmoleub  24673  nmoid  24684  bl2ioo  24734  zcld  24756  divcnOLD  24811  divcn  24813  divccn  24818  divccnOLD  24820  cncfcdm  24845  divccncf  24853  icoopnst  24890  clmzlmvsca  25067  cph2ass  25167  tcphcph  25191  cfilfcls  25228  bcthlem2  25279  rrxmet  25362  rrxdstprj1  25363  rrxdsfi  25365  cldcss  25395  dvrec  25913  dvmptfsum  25933  aalioulem3  26296  taylply2  26329  taylply2OLD  26330  efsubm  26514  dchrelbasd  27204  dchrmulcl  27214  2sqreulem3  27418  pntrmax  27529  padicabv  27595  nosupbnd2  27682  noinfbnd2  27697  ssltd  27758  divsmulw  28162  axtgcont  28490  xmstrkgc  28907  axsegconlem1  28939  axlowdimlem15  28978  usgredg2vlem1  29247  usgredg2vlem2  29248  iswlkon  29678  wwlksnextsurj  29922  elwwlks2  29991  elwspths2spth  29992  frrusgrord  30365  numclwwlk1lem2foalem  30375  grpoidinvlem2  30529  grpoidinvlem3  30530  ablo4  30574  ablomuldiv  30576  nvaddsub4  30681  nvmeq0  30682  sspmval  30757  sspimsval  30762  lnosub  30783  dipsubdir  30872  hvadd4  31060  hvpncan  31063  his35  31112  hiassdi  31115  shscli  31341  shmodsi  31413  chj4  31559  spansnmul  31588  spansncol  31592  spanunsni  31603  hoadd4  31808  hosubadd4  31838  lnopl  31938  unopf1o  31940  counop  31945  lnfnl  31955  hmopadj2  31965  eighmre  31987  lnopmi  32024  lnophsi  32025  hmops  32044  hmopm  32045  cnlnadjlem2  32092  adjmul  32116  adjadd  32117  kbass6  32145  mdslj1i  32343  mdslj2i  32344  mdslmd1lem1  32349  mdslmd2i  32354  chirredlem3  32416  isoun  32730  xdivmul  32955  odutos  32999  lmodvslmhm  33082  isarchi2  33216  archiabllem2  33228  imasmhm  33384  imasghm  33385  imasrhm  33386  imaslmhm  33387  quslmhm  33389  tngdim  33719  fedgmullem2  33736  metider  34000  pl1cn  34061  rossros  34286  ismeas  34305  dya2iocnei  34388  inelcarsg  34417  signstfvc  34680  bnj563  34848  fisshasheq  35258  cnpconn  35373  cvmseu  35419  elmrsubrn  35663  mrsubco  35664  fneint  36491  fnessref  36500  tailfb  36520  onsucuni3  37511  pibt2  37561  ptrecube  37760  poimirlem4  37764  heicant  37795  mblfinlem1  37797  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  cnambfre  37808  itg2addnclem2  37812  ftc1anclem5  37837  ftc1anclem6  37838  metf1o  37895  isbnd3b  37925  equivbnd  37930  heiborlem3  37953  rrnmet  37969  rrndstprj1  37970  rrntotbnd  37976  exidcl  38016  ghomco  38031  ghomdiv  38032  grpokerinj  38033  rngoneglmul  38083  rngonegrmul  38084  rngosubdi  38085  rngosubdir  38086  isdrngo2  38098  rngohomco  38114  rngoisocnv  38121  riscer  38128  crngm4  38143  crngohomfo  38146  idlsubcl  38163  inidl  38170  keridl  38172  ispridlc  38210  pridlc3  38213  dmncan1  38216  lflvscl  39276  3dim0  39656  linepsubN  39951  cdlemg2fvlem  40793  trlcoat  40922  istendod  40961  dva1dim  41184  dvhvaddcomN  41295  dihf11  41466  dihlatat  41536  sn-sup2  42688  fsuppssind  42778  mhphf  42782  ismrc  42885  isnacs3  42894  mzpindd  42930  pellex  43019  monotoddzzfi  43126  lermxnn0  43134  rmyeq0  43137  rmyeq  43138  lermy  43139  jm2.27  43192  lsmfgcl  43258  fsumcnsrcl  43350  rngunsnply  43353  gsumws3  44379  mnringmulrcld  44411  nzin  44501  ofdivrec  44509  ofdivcan4  44510  chordthmALT  45115  wessf1ornlem  45371  projf1o  45383  ltdiv23neg  45580  fmulcl  45769  prproropf1olem2  47692  prproropf1olem4  47694  mgmplusgiopALT  48382  itsclc0xyqsolb  48958  toslat  49169  cicerALT  49233