Theorem 3expb 1138

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expia  1139  3adant3r1  1201  3adant3r2  1202  3adant3r3  1203  mp3an1  1477  sotri  6129  fnfco  6747  mpoeq3dva  7496  oprres  7587  fovcdmda  7591  fnmpoovd  8088  offval22  8089  bropfvvvvlem  8092  fnsuppres  8193  suppsssn  8203  sprmpod  8226  oaass  8552  omlimcl  8569  odi  8570  nnmsucr  8617  nnasmo  8655  unfi  9162  ttrclse  9703  cflim2  10262  mulcanenq  10962  mul4  11395  add4  11448  2addsub  11488  addsubeq4  11489  subadd4  11519  muladd  11663  ltleadd  11714  divmul  11892  divne0  11901  div23  11908  div12  11911  div11  11917  divsubdir  11925  subdivcomb1  11927  divcan5  11934  divmuleq  11937  divcan6  11939  divdiv32  11940  div2sub  12057  letrp1  12076  lemul12b  12089  lediv1  12097  lt2mul2div  12110  lemuldiv  12112  ltdiv2  12118  ledivdiv  12121  lediv2  12122  ltdiv23  12123  lediv23  12124  sup2  12188  cju  12231  nndivre  12294  nndivtr  12300  nn0addge1  12567  nn0addge2  12568  peano2uz2  12702  uzind  12706  uzind3  12708  fzind  12712  fnn0ind  12713  uzind4  12948  qre  12995  irrmul  13016  rpdivcl  13061  rerpdivcl  13066  xrinfmsslem  13352  ixxin  13407  iccshftr  13531  iccshftl  13533  iccdil  13535  icccntr  13537  fzaddel  13605  fzadd2  13606  fzrev  13634  modlt  13933  modcyc  13959  axdc4uzlem  14039  expdiv  14169  fundmge2nop0  14559  swrd00  14704  swrdcl  14705  swrdnnn0nd  14718  swrd0  14720  swrdwrdsymb  14724  ccatpfx  14762  swrdccat  14796  splid  14814  swrdco  14900  2shfti  15143  isermulc2  15735  fsummulc2  15860  dvdscmulr  16366  dvdsmulcr  16367  dvds2add  16372  dvds2sub  16373  dvdstr  16376  alzdvds  16402  divalg2  16487  dvdslegcd  16586  lcmgcdlem  16688  lcmgcdeq  16694  isprm6  16797  pcqcl  16940  vdwmc2  17063  ressinbas  17329  cicer  17887  isposd  18402  pleval2i  18414  poslubmo  18489  posglbmo  18490  tosso  18497  mgmplusf  18732  mgmn0plusgf  18733  ismgmd  18736  grpinva  18760  idmgmhm  18793  resmgmhm  18803  resmgmhm2  18804  resmgmhm2b  18805  mgmhmco  18806  mgmhmima  18807  submgmacs  18809  sgrpidmnd  18831  ismndd  18849  imasmnd2  18871  idmhm  18892  mndvcl  18894  issubm2  18901  0mhm  18917  resmhm  18918  resmhm2  18919  resmhm2b  18920  mhmco  18921  mhmimalem  18922  submacs  18925  prdspjmhm  18927  pwsdiagmhm  18929  pwsco1mhm  18930  pwsco2mhm  18931  gsumwsubmcl  18935  gsumsgrpccat  18938  gsumwmhm  18943  grpinvcnv  19119  grpinvnzcl  19123  grpsubf  19131  imasgrp2  19167  qusgrp2  19170  mhmfmhm  19177  mulgnnsubcl  19198  mulgnndir  19215  issubg4  19258  isnsg3  19272  nsgacs  19274  nsgid  19282  qusadd  19305  qus0subgadd  19316  ghmmhm  19342  ghmmhmb  19343  idghm  19347  resghm  19348  ghmf1  19362  qusghm  19371  gaid  19415  subgga  19416  gasubg  19418  invoppggim  19476  gsmsymgrfix  19544  smndlsmidm  19772  pj1ghm  19819  mulgnn0di  19941  mulgmhm  19943  mulgghm  19944  ghmfghm  19946  invghm  19949  ghmplusg  19962  ablnsg  19963  qusabl  19981  gsumval3eu  20020  gsumval3  20023  gsumzcl2  20026  gsumzaddlem  20037  gsumzadd  20038  gsumzmhm  20053  gsumzoppg  20060  srgfcl  20324  srgcom4lem  20341  srgmulgass  20345  srglmhm  20349  srgrmhm  20350  ringcomlem  20409  ringlghm  20443  ringrghm  20444  pwspjmhmmgpd  20457  c0mgm  20589  c0mhm  20590  isnzr2  20667  subrngringnsg  20704  issubrng2  20709  rhmimasubrnglem  20716  issubrg2  20743  domnmuln0  20860  isdomn3  20865  isdrng3lem2  20904  issrngd  21010  islmodd  21039  lmodscaf  21057  lcomf  21074  lmodvsghm  21096  rmodislmodlem  21102  lssacs  21140  idlmhm  21214  invlmhm  21215  lmhmvsca  21218  reslmhm2  21226  reslmhm2b  21227  pwsdiaglmhm  21230  pwssplit2  21233  pwssplit3  21234  issubrgd  21362  qusrhm  21467  qusmul2idl  21470  crngridl  21471  qusmulrng  21474  cmprmidlmcl  21527  expmhm  21638  zntoslem  21758  znfld  21762  psgnghm  21782  phlipf  21854  frlmup1  22000  asclghm  22084  asclrhm  22092  rnasclmulcl  22096  psraddcl  22141  psrvscacl  22153  psrass23  22170  psrbagev1  22280  coe1sclmulfv  22496  cply1mul  22508  evls1fpws  22581  rhmply1vsca  22597  matbas2d  22632  submaeval  22791  minmar1eval  22858  cpmatacl  22925  pmatcollpw1  22985  pmatcollpw  22990  tgclb  23179  topbas  23181  ntrss  23264  mretopd  23301  neissex  23336  cnpnei  23473  lmcnp  23513  ordthaus  23593  llynlly  23687  restnlly  23692  llyidm  23698  nllyidm  23699  ptbasin  23787  txcnp  23830  ist0-4  23939  kqt0lem  23946  isr0  23947  regr1lem2  23950  cmphmph  23998  connhmph  23999  fbun  24050  trfbas2  24053  isfil2  24066  isfild  24068  infil  24073  fbasfip  24078  fbasrn  24094  trfil2  24097  rnelfmlem  24162  fmfnfmlem3  24166  flimopn  24185  txflf  24216  fclsnei  24229  fclsfnflim  24237  fcfnei  24245  clssubg  24319  tgphaus  24327  qustgplem  24331  tsmsadd  24357  psmetxrge0  24523  psmetlecl  24525  xmetlecl  24556  xmettpos  24559  imasdsf1olem  24583  imasf1oxmet  24585  imasf1omet  24586  elbl3ps  24601  elbl3  24602  metss  24718  comet  24723  stdbdxmet  24725  stdbdmet  24726  methaus  24730  nrmmetd  24784  abvmet  24785  isngp4  24822  subgngp  24845  nmoi2  24940  nmoleub  24941  nmoid  24952  bl2ioo  25002  zcld  25024  divcn  25080  divccn  25085  cncfcdm  25110  divccncf  25118  icoopnst  25151  clmzlmvsca  25325  cph2ass  25425  tcphcph  25449  cfilfcls  25486  bcthlem2  25537  rrxmet  25620  rrxdstprj1  25621  rrxdsfi  25623  cldcss  25653  dvrec  26167  dvmptfsum  26187  aalioulem3  26550  taylply2  26584  efsubm  26769  dchrelbasd  27456  dchrmulcl  27466  2sqreulem3  27670  pntrmax  27781  padicabv  27847  nosupbnd2  27933  noinfbnd2  27948  sltsd  28014  divmulsw  28439  axtgcont  28791  xmstrkgc  29292  axsegconlem1  29324  axlowdimlem15  29363  usgredg2vlem1  29635  usgredg2vlem2  29636  iswlkon  30065  wwlksnextsurj  30318  elwwlks2  30387  elwspths2spth  30388  frrusgrord  30765  numclwwlk1lem2foalem  30775  grpoidinvlem2  30930  grpoidinvlem3  30931  ablo4  30975  ablomuldiv  30977  nvaddsub4  31082  nvmeq0  31083  sspmval  31158  sspimsval  31163  lnosub  31184  dipsubdir  31273  hvadd4  31461  hvpncan  31464  his35  31513  hiassdi  31516  shscli  31742  shmodsi  31814  chj4  31960  spansnmul  31989  spansncol  31993  spanunsni  32004  hoadd4  32209  hosubadd4  32239  lnopl  32339  unopf1o  32341  counop  32346  lnfnl  32356  hmopadj2  32366  eighmre  32388  lnopmi  32425  lnophsi  32426  hmops  32445  hmopm  32446  cnlnadjlem2  32493  adjmul  32517  adjadd  32518  kbass6  32546  mdslj1i  32744  mdslj2i  32745  mdslmd1lem1  32750  mdslmd2i  32755  chirredlem3  32817  isoun  33120  xdivmul  33316  odutos  33354  lmodvslmhm  33436  isarchi2  33571  archiabllem2  33583  imasmhm  33740  imasghm  33741  imasrhm  33742  imaslmhm  33743  quslmhm  33745  tngdim  34069  fedgmullem2  34086  metider  34350  pl1cn  34411  rossros  34637  ismeas  34656  dya2iocnei  34739  inelcarsg  34768  signstfvc  35028  bnj563  35199  fisshasheq  35663  cnpconn  35761  cvmseu  35807  elmrsubrn  36051  mrsubco  36052  fneint  36918  fnessref  36927  tailfb  36947  onsucuni3  38072  pibt2  38122  ptrecube  38330  poimirlem4  38334  heicant  38365  mblfinlem1  38367  mblfinlem2  38368  mblfinlem3  38369  mblfinlem4  38370  cnambfre  38378  itg2addnclem2  38382  ftc1anclem5  38407  ftc1anclem6  38408  metf1o  38466  isbnd3b  38496  equivbnd  38501  heiborlem3  38524  rrnmet  38540  rrndstprj1  38541  rrntotbnd  38547  exidcl  38587  ghomco  38602  ghomdiv  38603  grpokerinj  38604  rngoneglmul  38654  rngonegrmul  38655  rngosubdi  38656  rngosubdir  38657  isdrngo2  38669  rngohomco  38685  rngoisocnv  38692  riscer  38699  crngm4  38714  crngohomfo  38717  idlsubcl  38734  inidl  38741  keridl  38743  ispridlc  38781  pridlc3  38784  dmncan1  38787  lflvscl  39911  3dim0  40291  linepsubN  40586  cdlemg2fvlem  41428  trlcoat  41557  istendod  41596  dva1dim  41819  dvhvaddcomN  41930  dihf11  42101  dihlatat  42171  sn-sup2  43325  fsuppssind  43385  mhphf  43389  ismrc  43492  isnacs3  43501  mzpindd  43537  pellex  43622  monotoddzzfi  43729  lermxnn0  43737  rmyeq0  43740  rmyeq  43741  lermy  43742  jm2.27  43795  lsmfgcl  43861  fsumcnsrcl  43953  rngunsnply  43956  gsumws3  44982  mnringmulrcld  45012  nzin  45088  ofdivrec  45096  ofdivcan4  45097  chordthmALT  45701  wessf1ornlem  45963  projf1o  45974  ltdiv23neg  46169  fmulcl  46357  prproropf1olem2  48313  prproropf1olem4  48315  mgmplusgiopALT  49018  idomcanl  49171  itsclc0xyqsolb  49609  toslat  49819  cicerALT  49883