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  6092  fnfco  6707  mpoeq3dva  7445  oprres  7536  fovcdmda  7539  fnmpoovd  8039  offval22  8040  bropfvvvvlem  8043  fnsuppres  8143  suppsssn  8153  sprmpod  8176  oaass  8498  omlimcl  8515  odi  8516  nnmsucr  8563  nnasmo  8601  unfi  9107  ttrclse  9648  cflim2  10185  mulcanenq  10883  mul4  11313  add4  11366  2addsub  11406  addsubeq4  11407  subadd4  11437  muladd  11581  ltleadd  11632  divmul  11811  divne0  11820  div23  11827  div12  11830  div11  11836  divsubdir  11847  subdivcomb1  11848  divcan5  11855  divmuleq  11858  divcan6  11860  divdiv32  11861  div2sub  11978  letrp1  11997  lemul12b  12010  lediv1  12019  lt2mul2div  12032  lemuldiv  12034  ltdiv2  12040  ledivdiv  12043  lediv2  12044  ltdiv23  12045  lediv23  12046  sup2  12110  cju  12153  nndivre  12198  nndivtr  12204  nn0addge1  12459  nn0addge2  12460  peano2uz2  12592  uzind  12596  uzind3  12598  fzind  12602  fnn0ind  12603  uzind4  12831  qre  12878  irrmul  12899  rpdivcl  12944  rerpdivcl  12949  xrinfmsslem  13235  ixxin  13290  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzaddel  13486  fzadd2  13487  fzrev  13515  modlt  13812  modcyc  13838  axdc4uzlem  13918  expdiv  14048  fundmge2nop0  14437  swrd00  14580  swrdcl  14581  swrdnnn0nd  14592  swrd0  14594  swrdwrdsymb  14598  ccatpfx  14636  swrdccat  14670  splid  14688  swrdco  14772  2shfti  15015  isermulc2  15593  fsummulc2  15719  dvdscmulr  16223  dvdsmulcr  16224  dvds2add  16229  dvds2sub  16230  dvdstr  16233  alzdvds  16259  divalg2  16344  dvdslegcd  16443  lcmgcdlem  16545  lcmgcdeq  16551  isprm6  16653  pcqcl  16796  vdwmc2  16919  ressinbas  17184  cicer  17742  isposd  18257  pleval2i  18269  poslubmo  18344  posglbmo  18345  tosso  18352  mgmplusf  18587  ismgmd  18589  grpinva  18611  idmgmhm  18638  resmgmhm  18648  resmgmhm2  18649  resmgmhm2b  18650  mgmhmco  18651  mgmhmima  18652  submgmacs  18654  sgrpidmnd  18676  ismndd  18693  imasmnd2  18711  idmhm  18732  mndvcl  18734  issubm2  18741  0mhm  18756  resmhm  18757  resmhm2  18758  resmhm2b  18759  mhmco  18760  mhmimalem  18761  submacs  18764  prdspjmhm  18766  pwsdiagmhm  18768  pwsco1mhm  18769  pwsco2mhm  18770  gsumwsubmcl  18774  gsumsgrpccat  18777  gsumwmhm  18782  grpinvcnv  18951  grpinvnzcl  18956  grpsubf  18964  imasgrp2  19000  qusgrp2  19003  mhmfmhm  19010  mulgnnsubcl  19031  mulgnndir  19048  issubg4  19090  isnsg3  19104  nsgacs  19106  nsgid  19114  qusadd  19132  qus0subgadd  19143  ghmmhm  19170  ghmmhmb  19171  idghm  19175  resghm  19176  ghmf1  19190  qusghm  19199  gaid  19243  subgga  19244  gasubg  19246  invoppggim  19304  gsmsymgrfix  19372  smndlsmidm  19600  pj1ghm  19647  mulgnn0di  19769  mulgmhm  19771  mulgghm  19772  ghmfghm  19774  invghm  19777  ghmplusg  19790  ablnsg  19791  qusabl  19809  gsumval3eu  19848  gsumval3  19851  gsumzcl2  19854  gsumzaddlem  19865  gsumzadd  19866  gsumzmhm  19881  gsumzoppg  19888  srgfcl  20146  srgcom4lem  20163  srgmulgass  20167  srglmhm  20171  srgrmhm  20172  ringcomlem  20229  ringlghm  20262  ringrghm  20263  pwspjmhmmgpd  20278  c0mgm  20410  c0mhm  20411  isnzr2  20466  subrngringnsg  20501  issubrng2  20506  rhmimasubrnglem  20513  issubrg2  20540  domnmuln0  20657  isdomn3  20663  issrngd  20803  islmodd  20832  lmodscaf  20850  lcomf  20867  lmodvsghm  20889  rmodislmodlem  20895  lssacs  20933  idlmhm  21008  invlmhm  21009  lmhmvsca  21012  reslmhm2  21020  reslmhm2b  21021  pwsdiaglmhm  21024  pwssplit2  21027  pwssplit3  21028  issubrgd  21156  qusrhm  21246  qusmul2idl  21249  crngridl  21250  qusmulrng  21252  expmhm  21406  zntoslem  21526  znfld  21530  psgnghm  21550  phlipf  21622  frlmup1  21768  asclghm  21853  asclrhm  21861  rnasclmulcl  21865  psraddcl  21909  psraddclOLD  21910  psrvscacl  21922  psrass23  21939  psrbagev1  22047  coe1sclmulfv  22240  cply1mul  22255  evls1fpws  22328  rhmply1vsca  22347  matbas2d  22382  submaeval  22541  minmar1eval  22608  cpmatacl  22675  pmatcollpw1  22735  pmatcollpw  22740  tgclb  22929  topbas  22931  ntrss  23014  mretopd  23051  neissex  23086  cnpnei  23223  lmcnp  23263  ordthaus  23343  llynlly  23436  restnlly  23441  llyidm  23447  nllyidm  23448  ptbasin  23536  txcnp  23579  ist0-4  23688  kqt0lem  23695  isr0  23696  regr1lem2  23699  cmphmph  23747  connhmph  23748  fbun  23799  trfbas2  23802  isfil2  23815  isfild  23817  infil  23822  fbasfip  23827  fbasrn  23843  trfil2  23846  rnelfmlem  23911  fmfnfmlem3  23915  flimopn  23934  txflf  23965  fclsnei  23978  fclsfnflim  23986  fcfnei  23994  clssubg  24068  tgphaus  24076  qustgplem  24080  tsmsadd  24106  psmetxrge0  24272  psmetlecl  24274  xmetlecl  24305  xmettpos  24308  imasdsf1olem  24332  imasf1oxmet  24334  imasf1omet  24335  elbl3ps  24350  elbl3  24351  metss  24467  comet  24472  stdbdxmet  24474  stdbdmet  24475  methaus  24479  nrmmetd  24533  abvmet  24534  isngp4  24571  subgngp  24594  nmoi2  24689  nmoleub  24690  nmoid  24701  bl2ioo  24751  zcld  24773  divcnOLD  24828  divcn  24830  divccn  24835  divccnOLD  24837  cncfcdm  24862  divccncf  24870  icoopnst  24907  clmzlmvsca  25084  cph2ass  25184  tcphcph  25208  cfilfcls  25245  bcthlem2  25296  rrxmet  25379  rrxdstprj1  25380  rrxdsfi  25382  cldcss  25412  dvrec  25930  dvmptfsum  25950  aalioulem3  26313  taylply2  26346  taylply2OLD  26347  efsubm  26531  dchrelbasd  27221  dchrmulcl  27231  2sqreulem3  27435  pntrmax  27546  padicabv  27612  nosupbnd2  27699  noinfbnd2  27714  sltsd  27779  divmulsw  28204  axtgcont  28557  xmstrkgc  28974  axsegconlem1  29006  axlowdimlem15  29045  usgredg2vlem1  29314  usgredg2vlem2  29315  iswlkon  29745  wwlksnextsurj  29989  elwwlks2  30058  elwspths2spth  30059  frrusgrord  30432  numclwwlk1lem2foalem  30442  grpoidinvlem2  30597  grpoidinvlem3  30598  ablo4  30642  ablomuldiv  30644  nvaddsub4  30749  nvmeq0  30750  sspmval  30825  sspimsval  30830  lnosub  30851  dipsubdir  30940  hvadd4  31128  hvpncan  31131  his35  31180  hiassdi  31183  shscli  31409  shmodsi  31481  chj4  31627  spansnmul  31656  spansncol  31660  spanunsni  31671  hoadd4  31876  hosubadd4  31906  lnopl  32006  unopf1o  32008  counop  32013  lnfnl  32023  hmopadj2  32033  eighmre  32055  lnopmi  32092  lnophsi  32093  hmops  32112  hmopm  32113  cnlnadjlem2  32160  adjmul  32184  adjadd  32185  kbass6  32213  mdslj1i  32411  mdslj2i  32412  mdslmd1lem1  32417  mdslmd2i  32422  chirredlem3  32484  isoun  32796  xdivmul  33021  odutos  33065  lmodvslmhm  33148  isarchi2  33283  archiabllem2  33295  imasmhm  33451  imasghm  33452  imasrhm  33453  imaslmhm  33454  quslmhm  33456  tngdim  33795  fedgmullem2  33812  metider  34076  pl1cn  34137  rossros  34362  ismeas  34381  dya2iocnei  34464  inelcarsg  34493  signstfvc  34756  bnj563  34924  fisshasheq  35335  cnpconn  35450  cvmseu  35496  elmrsubrn  35740  mrsubco  35741  fneint  36568  fnessref  36577  tailfb  36597  onsucuni3  37626  pibt2  37676  ptrecube  37875  poimirlem4  37879  heicant  37910  mblfinlem1  37912  mblfinlem2  37913  mblfinlem3  37914  mblfinlem4  37915  cnambfre  37923  itg2addnclem2  37927  ftc1anclem5  37952  ftc1anclem6  37953  metf1o  38010  isbnd3b  38040  equivbnd  38045  heiborlem3  38068  rrnmet  38084  rrndstprj1  38085  rrntotbnd  38091  exidcl  38131  ghomco  38146  ghomdiv  38147  grpokerinj  38148  rngoneglmul  38198  rngonegrmul  38199  rngosubdi  38200  rngosubdir  38201  isdrngo2  38213  rngohomco  38229  rngoisocnv  38236  riscer  38243  crngm4  38258  crngohomfo  38261  idlsubcl  38278  inidl  38285  keridl  38287  ispridlc  38325  pridlc3  38328  dmncan1  38331  lflvscl  39457  3dim0  39837  linepsubN  40132  cdlemg2fvlem  40974  trlcoat  41103  istendod  41142  dva1dim  41365  dvhvaddcomN  41476  dihf11  41647  dihlatat  41717  sn-sup2  42865  fsuppssind  42955  mhphf  42959  ismrc  43062  isnacs3  43071  mzpindd  43107  pellex  43196  monotoddzzfi  43303  lermxnn0  43311  rmyeq0  43314  rmyeq  43315  lermy  43316  jm2.27  43369  lsmfgcl  43435  fsumcnsrcl  43527  rngunsnply  43530  gsumws3  44556  mnringmulrcld  44588  nzin  44678  ofdivrec  44686  ofdivcan4  44687  chordthmALT  45292  wessf1ornlem  45548  projf1o  45559  ltdiv23neg  45756  fmulcl  45945  prproropf1olem2  47868  prproropf1olem4  47870  mgmplusgiopALT  48558  itsclc0xyqsolb  49134  toslat  49345  cicerALT  49409