Theorem 3expb 1119

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 1118	. 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  1120  3adant3r1  1181  3adant3r2  1182  3adant3r3  1183  mp3an1  1447  sotri  6150  fnfco  6774  mpoeq3dva  7510  oprres  7601  fovcdmda  7604  fnmpoovd  8111  offval22  8112  bropfvvvvlem  8115  fnsuppres  8215  suppsssn  8225  sprmpod  8248  oaass  8598  omlimcl  8615  odi  8616  nnmsucr  8662  nnasmo  8700  unfi  9210  ttrclse  9765  cflim2  10301  mulcanenq  10998  mul4  11427  add4  11480  2addsub  11520  addsubeq4  11521  subadd4  11551  muladd  11693  ltleadd  11744  divmul  11923  divne0  11932  div23  11939  div12  11942  div11  11948  divsubdir  11959  subdivcomb1  11960  divcan5  11967  divmuleq  11970  divcan6  11972  divdiv32  11973  div2sub  12090  letrp1  12109  lemul12b  12122  lediv1  12131  lt2mul2div  12144  lemuldiv  12146  ltdiv2  12152  ledivdiv  12155  lediv2  12156  ltdiv23  12157  lediv23  12158  sup2  12222  cju  12260  nndivre  12305  nndivtr  12311  nn0addge1  12570  nn0addge2  12571  peano2uz2  12704  uzind  12708  uzind3  12710  fzind  12714  fnn0ind  12715  uzind4  12946  qre  12993  irrmul  13014  rpdivcl  13058  rerpdivcl  13063  xrinfmsslem  13347  ixxin  13401  iccshftr  13523  iccshftl  13525  iccdil  13527  icccntr  13529  fzaddel  13595  fzadd2  13596  fzrev  13624  modlt  13917  modcyc  13943  axdc4uzlem  14021  expdiv  14151  fundmge2nop0  14538  swrd00  14679  swrdcl  14680  swrdnnn0nd  14691  swrd0  14693  swrdwrdsymb  14697  ccatpfx  14736  swrdccat  14770  splid  14788  swrdco  14873  2shfti  15116  isermulc2  15691  fsummulc2  15817  dvdscmulr  16319  dvdsmulcr  16320  dvds2add  16324  dvds2sub  16325  dvdstr  16328  alzdvds  16354  divalg2  16439  dvdslegcd  16538  lcmgcdlem  16640  lcmgcdeq  16646  isprm6  16748  pcqcl  16890  vdwmc2  17013  ressinbas  17291  cicer  17854  isposd  18381  pleval2i  18394  poslubmo  18469  posglbmo  18470  tosso  18477  mgmplusf  18676  ismgmd  18678  grpinva  18700  idmgmhm  18727  resmgmhm  18737  resmgmhm2  18738  resmgmhm2b  18739  mgmhmco  18740  mgmhmima  18741  submgmacs  18743  sgrpidmnd  18765  ismndd  18782  imasmnd2  18800  idmhm  18821  mndvcl  18823  issubm2  18830  0mhm  18845  resmhm  18846  resmhm2  18847  resmhm2b  18848  mhmco  18849  mhmimalem  18850  submacs  18853  prdspjmhm  18855  pwsdiagmhm  18857  pwsco1mhm  18858  pwsco2mhm  18859  gsumwsubmcl  18863  gsumsgrpccat  18866  gsumwmhm  18871  grpinvcnv  19037  grpinvnzcl  19042  grpsubf  19050  imasgrp2  19086  qusgrp2  19089  mhmfmhm  19096  mulgnnsubcl  19117  mulgnndir  19134  issubg4  19176  isnsg3  19191  nsgacs  19193  nsgid  19201  qusadd  19219  qus0subgadd  19230  ghmmhm  19257  ghmmhmb  19258  idghm  19262  resghm  19263  ghmf1  19277  qusghm  19286  gaid  19330  subgga  19331  gasubg  19333  invoppggim  19394  gsmsymgrfix  19461  smndlsmidm  19689  pj1ghm  19736  mulgnn0di  19858  mulgmhm  19860  mulgghm  19861  ghmfghm  19863  invghm  19866  ghmplusg  19879  ablnsg  19880  qusabl  19898  gsumval3eu  19937  gsumval3  19940  gsumzcl2  19943  gsumzaddlem  19954  gsumzadd  19955  gsumzmhm  19970  gsumzoppg  19977  srgfcl  20214  srgcom4lem  20231  srgmulgass  20235  srglmhm  20239  srgrmhm  20240  ringcomlem  20293  ringlghm  20326  ringrghm  20327  pwspjmhmmgpd  20342  c0mgm  20476  c0mhm  20477  isnzr2  20535  subrngringnsg  20570  issubrng2  20575  rhmimasubrnglem  20582  issubrg2  20609  domnmuln0  20726  isdomn3  20732  issrngd  20873  islmodd  20881  lmodscaf  20899  lcomf  20916  lmodvsghm  20938  rmodislmodlem  20944  lssacs  20983  idlmhm  21058  invlmhm  21059  lmhmvsca  21062  reslmhm2  21070  reslmhm2b  21071  pwsdiaglmhm  21074  pwssplit2  21077  pwssplit3  21078  issubrgd  21214  qusrhm  21304  qusmul2idl  21307  crngridl  21308  qusmulrng  21310  expmhm  21472  zntoslem  21593  znfld  21597  psgnghm  21616  phlipf  21688  frlmup1  21836  asclghm  21921  asclrhm  21928  rnasclmulcl  21932  psraddcl  21976  psraddclOLD  21977  psrvscacl  21989  psrass23  22007  psrbagev1  22119  coe1sclmulfv  22302  cply1mul  22316  evls1fpws  22389  rhmply1vsca  22408  matbas2d  22445  submaeval  22604  minmar1eval  22671  cpmatacl  22738  pmatcollpw1  22798  pmatcollpw  22803  tgclb  22993  topbas  22995  ntrss  23079  mretopd  23116  neissex  23151  cnpnei  23288  lmcnp  23328  ordthaus  23408  llynlly  23501  restnlly  23506  llyidm  23512  nllyidm  23513  ptbasin  23601  txcnp  23644  ist0-4  23753  kqt0lem  23760  isr0  23761  regr1lem2  23764  cmphmph  23812  connhmph  23813  fbun  23864  trfbas2  23867  isfil2  23880  isfild  23882  infil  23887  fbasfip  23892  fbasrn  23908  trfil2  23911  rnelfmlem  23976  fmfnfmlem3  23980  flimopn  23999  txflf  24030  fclsnei  24043  fclsfnflim  24051  fcfnei  24059  clssubg  24133  tgphaus  24141  qustgplem  24145  tsmsadd  24171  psmetxrge0  24339  psmetlecl  24341  xmetlecl  24372  xmettpos  24375  imasdsf1olem  24399  imasf1oxmet  24401  imasf1omet  24402  elbl3ps  24417  elbl3  24418  metss  24537  comet  24542  stdbdxmet  24544  stdbdmet  24545  methaus  24549  nrmmetd  24603  abvmet  24604  isngp4  24641  subgngp  24664  nmoi2  24767  nmoleub  24768  nmoid  24779  bl2ioo  24828  zcld  24849  divcnOLD  24904  divcn  24906  divccn  24911  divccnOLD  24913  cncfcdm  24938  divccncf  24946  icoopnst  24983  clmzlmvsca  25160  cph2ass  25261  tcphcph  25285  cfilfcls  25322  bcthlem2  25373  rrxmet  25456  rrxdstprj1  25457  rrxdsfi  25459  cldcss  25489  dvrec  26008  dvmptfsum  26028  aalioulem3  26391  taylply2  26424  taylply2OLD  26425  efsubm  26608  dchrelbasd  27298  dchrmulcl  27308  2sqreulem3  27512  pntrmax  27623  padicabv  27689  nosupbnd2  27776  noinfbnd2  27791  ssltd  27851  divsmulw  28233  axtgcont  28492  xmstrkgc  28915  axsegconlem1  28947  axlowdimlem15  28986  usgredg2vlem1  29257  usgredg2vlem2  29258  iswlkon  29690  wwlksnextsurj  29930  elwwlks2  29996  elwspths2spth  29997  frrusgrord  30370  numclwwlk1lem2foalem  30380  grpoidinvlem2  30534  grpoidinvlem3  30535  ablo4  30579  ablomuldiv  30581  nvaddsub4  30686  nvmeq0  30687  sspmval  30762  sspimsval  30767  lnosub  30788  dipsubdir  30877  hvadd4  31065  hvpncan  31068  his35  31117  hiassdi  31120  shscli  31346  shmodsi  31418  chj4  31564  spansnmul  31593  spansncol  31597  spanunsni  31608  hoadd4  31813  hosubadd4  31843  lnopl  31943  unopf1o  31945  counop  31950  lnfnl  31960  hmopadj2  31970  eighmre  31992  lnopmi  32029  lnophsi  32030  hmops  32049  hmopm  32050  cnlnadjlem2  32097  adjmul  32121  adjadd  32122  kbass6  32150  mdslj1i  32348  mdslj2i  32349  mdslmd1lem1  32354  mdslmd2i  32359  chirredlem3  32421  isoun  32717  xdivmul  32892  odutos  32943  lmodvslmhm  33036  isarchi2  33175  archiabllem2  33187  imasmhm  33362  imasghm  33363  imasrhm  33364  imaslmhm  33365  quslmhm  33367  tngdim  33641  fedgmullem2  33658  metider  33855  pl1cn  33916  rossros  34161  ismeas  34180  dya2iocnei  34264  inelcarsg  34293  signstfvc  34568  bnj563  34736  fisshasheq  35099  cnpconn  35215  cvmseu  35261  elmrsubrn  35505  mrsubco  35506  fneint  36331  fnessref  36340  tailfb  36360  onsucuni3  37350  pibt2  37400  ptrecube  37607  poimirlem4  37611  heicant  37642  mblfinlem1  37644  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  cnambfre  37655  itg2addnclem2  37659  ftc1anclem5  37684  ftc1anclem6  37685  metf1o  37742  isbnd3b  37772  equivbnd  37777  heiborlem3  37800  rrnmet  37816  rrndstprj1  37817  rrntotbnd  37823  exidcl  37863  ghomco  37878  ghomdiv  37879  grpokerinj  37880  rngoneglmul  37930  rngonegrmul  37931  rngosubdi  37932  rngosubdir  37933  isdrngo2  37945  rngohomco  37961  rngoisocnv  37968  riscer  37975  crngm4  37990  crngohomfo  37993  idlsubcl  38010  inidl  38017  keridl  38019  ispridlc  38057  pridlc3  38060  dmncan1  38063  lflvscl  39059  3dim0  39440  linepsubN  39735  cdlemg2fvlem  40577  trlcoat  40706  istendod  40745  dva1dim  40968  dvhvaddcomN  41079  dihf11  41250  dihlatat  41320  metakunt12  42198  sn-sup2  42478  fsuppssind  42580  mhphf  42584  ismrc  42689  isnacs3  42698  mzpindd  42734  pellex  42823  monotoddzzfi  42931  lermxnn0  42939  rmyeq0  42942  rmyeq  42943  lermy  42944  jm2.27  42997  lsmfgcl  43063  fsumcnsrcl  43155  rngunsnply  43158  gsumws3  44186  mnringmulrcld  44224  nzin  44314  ofdivrec  44322  ofdivcan4  44323  chordthmALT  44931  wessf1ornlem  45128  projf1o  45140  ltdiv23neg  45344  fmulcl  45537  prproropf1olem2  47429  prproropf1olem4  47431  mgmplusgiopALT  48038  itsclc0xyqsolb  48620  toslat  48771