Theorem 3expb 1126

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

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

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 1094

This theorem is referenced by:  3expia  1127  3adant3r1  1189  3adant3r2  1190  3adant3r3  1191  mp3an1  1456  sotri  6077  fnfco  6692  mpoeq3dva  7433  oprres  7524  fovcdmda  7527  fnmpoovd  8026  offval22  8027  bropfvvvvlem  8030  fnsuppres  8131  suppsssn  8141  sprmpod  8164  oaass  8486  omlimcl  8503  odi  8504  nnmsucr  8551  nnasmo  8589  unfi  9095  ttrclse  9639  cflim2  10176  mulcanenq  10874  mul4  11305  add4  11358  2addsub  11398  addsubeq4  11399  subadd4  11429  muladd  11573  ltleadd  11624  divmul  11803  divne0  11812  div23  11819  div12  11822  div11  11828  divsubdir  11839  subdivcomb1  11841  divcan5  11848  divmuleq  11851  divcan6  11853  divdiv32  11854  div2sub  11971  letrp1  11990  lemul12b  12003  lediv1  12012  lt2mul2div  12025  lemuldiv  12027  ltdiv2  12033  ledivdiv  12036  lediv2  12037  ltdiv23  12038  lediv23  12039  sup2  12103  cju  12146  nndivre  12209  nndivtr  12215  nn0addge1  12474  nn0addge2  12475  peano2uz2  12608  uzind  12612  uzind3  12614  fzind  12618  fnn0ind  12619  uzind4  12847  qre  12894  irrmul  12915  rpdivcl  12960  rerpdivcl  12965  xrinfmsslem  13251  ixxin  13306  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzaddel  13503  fzadd2  13504  fzrev  13532  modlt  13830  modcyc  13856  axdc4uzlem  13936  expdiv  14066  fundmge2nop0  14455  swrd00  14598  swrdcl  14599  swrdnnn0nd  14610  swrd0  14612  swrdwrdsymb  14616  ccatpfx  14654  swrdccat  14688  splid  14706  swrdco  14790  2shfti  15033  isermulc2  15611  fsummulc2  15737  dvdscmulr  16244  dvdsmulcr  16245  dvds2add  16250  dvds2sub  16251  dvdstr  16254  alzdvds  16280  divalg2  16365  dvdslegcd  16464  lcmgcdlem  16566  lcmgcdeq  16572  isprm6  16675  pcqcl  16818  vdwmc2  16941  ressinbas  17206  cicer  17764  isposd  18279  pleval2i  18291  poslubmo  18366  posglbmo  18367  tosso  18374  mgmplusf  18609  ismgmd  18611  grpinva  18633  idmgmhm  18660  resmgmhm  18670  resmgmhm2  18671  resmgmhm2b  18672  mgmhmco  18673  mgmhmima  18674  submgmacs  18676  sgrpidmnd  18698  ismndd  18715  imasmnd2  18733  idmhm  18754  mndvcl  18756  issubm2  18763  0mhm  18778  resmhm  18779  resmhm2  18780  resmhm2b  18781  mhmco  18782  mhmimalem  18783  submacs  18786  prdspjmhm  18788  pwsdiagmhm  18790  pwsco1mhm  18791  pwsco2mhm  18792  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  grpinvcnv  18973  grpinvnzcl  18978  grpsubf  18986  imasgrp2  19022  qusgrp2  19025  mhmfmhm  19032  mulgnnsubcl  19053  mulgnndir  19070  issubg4  19112  isnsg3  19126  nsgacs  19128  nsgid  19136  qusadd  19154  qus0subgadd  19165  ghmmhm  19192  ghmmhmb  19193  idghm  19197  resghm  19198  ghmf1  19212  qusghm  19221  gaid  19265  subgga  19266  gasubg  19268  invoppggim  19326  gsmsymgrfix  19394  smndlsmidm  19622  pj1ghm  19669  mulgnn0di  19791  mulgmhm  19793  mulgghm  19794  ghmfghm  19796  invghm  19799  ghmplusg  19812  ablnsg  19813  qusabl  19831  gsumval3eu  19870  gsumval3  19873  gsumzcl2  19876  gsumzaddlem  19887  gsumzadd  19888  gsumzmhm  19903  gsumzoppg  19910  srgfcl  20168  srgcom4lem  20185  srgmulgass  20189  srglmhm  20193  srgrmhm  20194  ringcomlem  20251  ringlghm  20284  ringrghm  20285  pwspjmhmmgpd  20298  c0mgm  20430  c0mhm  20431  isnzr2  20490  subrngringnsg  20525  issubrng2  20530  rhmimasubrnglem  20537  issubrg2  20564  domnmuln0  20681  isdomn3  20687  issrngd  20827  islmodd  20856  lmodscaf  20874  lcomf  20891  lmodvsghm  20913  rmodislmodlem  20919  lssacs  20957  idlmhm  21031  invlmhm  21032  lmhmvsca  21035  reslmhm2  21043  reslmhm2b  21044  pwsdiaglmhm  21047  pwssplit2  21050  pwssplit3  21051  issubrgd  21179  qusrhm  21269  qusmul2idl  21272  crngridl  21273  qusmulrng  21275  expmhm  21411  zntoslem  21531  znfld  21535  psgnghm  21555  phlipf  21627  frlmup1  21773  asclghm  21857  asclrhm  21865  rnasclmulcl  21869  psraddcl  21914  psrvscacl  21926  psrass23  21943  psrbagev1  22053  coe1sclmulfv  22269  cply1mul  22282  evls1fpws  22355  rhmply1vsca  22371  matbas2d  22406  submaeval  22565  minmar1eval  22632  cpmatacl  22699  pmatcollpw1  22759  pmatcollpw  22764  tgclb  22953  topbas  22955  ntrss  23038  mretopd  23075  neissex  23110  cnpnei  23247  lmcnp  23287  ordthaus  23367  llynlly  23460  restnlly  23465  llyidm  23471  nllyidm  23472  ptbasin  23560  txcnp  23603  ist0-4  23712  kqt0lem  23719  isr0  23720  regr1lem2  23723  cmphmph  23771  connhmph  23772  fbun  23823  trfbas2  23826  isfil2  23839  isfild  23841  infil  23846  fbasfip  23851  fbasrn  23867  trfil2  23870  rnelfmlem  23935  fmfnfmlem3  23939  flimopn  23958  txflf  23989  fclsnei  24002  fclsfnflim  24010  fcfnei  24018  clssubg  24092  tgphaus  24100  qustgplem  24104  tsmsadd  24130  psmetxrge0  24296  psmetlecl  24298  xmetlecl  24329  xmettpos  24332  imasdsf1olem  24356  imasf1oxmet  24358  imasf1omet  24359  elbl3ps  24374  elbl3  24375  metss  24491  comet  24496  stdbdxmet  24498  stdbdmet  24499  methaus  24503  nrmmetd  24557  abvmet  24558  isngp4  24595  subgngp  24618  nmoi2  24713  nmoleub  24714  nmoid  24725  bl2ioo  24775  zcld  24797  divcn  24853  divccn  24858  cncfcdm  24883  divccncf  24891  icoopnst  24924  clmzlmvsca  25098  cph2ass  25198  tcphcph  25222  cfilfcls  25259  bcthlem2  25310  rrxmet  25393  rrxdstprj1  25394  rrxdsfi  25396  cldcss  25426  dvrec  25940  dvmptfsum  25960  aalioulem3  26318  taylply2  26351  efsubm  26533  dchrelbasd  27220  dchrmulcl  27230  2sqreulem3  27434  pntrmax  27545  padicabv  27611  nosupbnd2  27698  noinfbnd2  27713  sltsd  27778  divmulsw  28203  axtgcont  28555  xmstrkgc  28972  axsegconlem1  29004  axlowdimlem15  29043  usgredg2vlem1  29312  usgredg2vlem2  29313  iswlkon  29742  wwlksnextsurj  29986  elwwlks2  30055  elwspths2spth  30056  frrusgrord  30429  numclwwlk1lem2foalem  30439  grpoidinvlem2  30594  grpoidinvlem3  30595  ablo4  30639  ablomuldiv  30641  nvaddsub4  30746  nvmeq0  30747  sspmval  30822  sspimsval  30827  lnosub  30848  dipsubdir  30937  hvadd4  31125  hvpncan  31128  his35  31177  hiassdi  31180  shscli  31406  shmodsi  31478  chj4  31624  spansnmul  31653  spansncol  31657  spanunsni  31668  hoadd4  31873  hosubadd4  31903  lnopl  32003  unopf1o  32005  counop  32010  lnfnl  32020  hmopadj2  32030  eighmre  32052  lnopmi  32089  lnophsi  32090  hmops  32109  hmopm  32110  cnlnadjlem2  32157  adjmul  32181  adjadd  32182  kbass6  32210  mdslj1i  32408  mdslj2i  32409  mdslmd1lem1  32414  mdslmd2i  32419  chirredlem3  32481  isoun  32794  xdivmul  33003  odutos  33047  lmodvslmhm  33131  isarchi2  33266  archiabllem2  33278  imasmhm  33437  imasghm  33438  imasrhm  33439  imaslmhm  33440  quslmhm  33442  tngdim  33797  fedgmullem2  33814  metider  34078  pl1cn  34139  rossros  34364  ismeas  34383  dya2iocnei  34466  inelcarsg  34495  signstfvc  34758  bnj563  34926  fisshasheq  35343  cnpconn  35458  cvmseu  35504  elmrsubrn  35748  mrsubco  35749  fneint  36576  fnessref  36585  tailfb  36605  onsucuni3  37729  pibt2  37779  ptrecube  37987  poimirlem4  37991  heicant  38022  mblfinlem1  38024  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  cnambfre  38035  itg2addnclem2  38039  ftc1anclem5  38064  ftc1anclem6  38065  metf1o  38122  isbnd3b  38152  equivbnd  38157  heiborlem3  38180  rrnmet  38196  rrndstprj1  38197  rrntotbnd  38203  exidcl  38243  ghomco  38258  ghomdiv  38259  grpokerinj  38260  rngoneglmul  38310  rngonegrmul  38311  rngosubdi  38312  rngosubdir  38313  isdrngo2  38325  rngohomco  38341  rngoisocnv  38348  riscer  38355  crngm4  38370  crngohomfo  38373  idlsubcl  38390  inidl  38397  keridl  38399  ispridlc  38437  pridlc3  38440  dmncan1  38443  lflvscl  39569  3dim0  39949  linepsubN  40244  cdlemg2fvlem  41086  trlcoat  41215  istendod  41254  dva1dim  41477  dvhvaddcomN  41588  dihf11  41759  dihlatat  41829  sn-sup2  42981  fsuppssind  43043  mhphf  43047  ismrc  43150  isnacs3  43159  mzpindd  43195  pellex  43280  monotoddzzfi  43387  lermxnn0  43395  rmyeq0  43398  rmyeq  43399  lermy  43400  jm2.27  43453  lsmfgcl  43519  fsumcnsrcl  43611  rngunsnply  43614  gsumws3  44640  mnringmulrcld  44672  nzin  44762  ofdivrec  44770  ofdivcan4  44771  chordthmALT  45376  wessf1ornlem  45632  projf1o  45643  ltdiv23neg  45838  fmulcl  46026  prproropf1olem2  47979  prproropf1olem4  47981  mgmplusgiopALT  48685  itsclc0xyqsolb  49261  toslat  49472  cicerALT  49536