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  6121  fnfco  6747  mpoeq3dva  7497  oprres  7588  fovcdmda  7592  fnmpoovd  8098  offval22  8099  bropfvvvvlem  8102  fnsuppres  8208  suppsssn  8218  sprmpod  8241  oaass  8569  omlimcl  8586  odi  8587  nnmsucr  8634  nnasmo  8672  unfi  9186  ttrclse  9728  cflim2  10341  mulcanenq  11045  mul4  11478  add4  11531  2addsub  11571  addsubeq4  11572  subadd4  11602  muladd  11748  ltleadd  11799  divmul  11977  divne0  11986  div23  11993  div12  11996  div11  12002  divsubdir  12010  subdivcomb1  12012  divcan5  12019  divmuleq  12022  divcan6  12024  divdiv32  12025  div2sub  12142  letrp1  12161  lemul12b  12174  lediv1  12182  lt2mul2div  12195  lemuldiv  12197  ltdiv2  12203  ledivdiv  12206  lediv2  12207  ltdiv23  12208  lediv23  12209  sup2  12273  cju  12316  nndivre  12379  nndivtr  12385  nn0addge1  12652  nn0addge2  12653  peano2uz2  12787  uzind  12791  uzind3  12793  fzind  12797  fnn0ind  12798  uzind4  13033  qre  13080  irrmul  13102  rpdivcl  13147  rerpdivcl  13152  xrinfmsslem  13438  ixxin  13493  iccshftr  13617  iccshftl  13619  iccdil  13621  icccntr  13623  fzaddel  13692  fzadd2  13693  fzrev  13721  modlt  14020  modcyc  14046  axdc4uzlem  14126  expdiv  14256  fundmge2nop0  14647  swrd00  14792  swrdcl  14793  swrdnnn0nd  14806  swrd0  14808  swrdwrdsymb  14812  ccatpfx  14850  swrdccat  14884  splid  14902  swrdco  14988  2shfti  15233  isermulc2  15825  fsummulc2  15950  dvdscmulr  16454  dvdsmulcr  16455  dvds2add  16460  dvds2sub  16461  dvdstr  16464  alzdvds  16490  divalg2  16575  dvdslegcd  16674  lcmgcdlem  16781  lcmgcdeq  16787  isprm6  16890  pcqcl  17034  vdwmc2  17157  ressinbas  17423  cicer  17981  isposd  18496  pleval2i  18508  poslubmo  18583  posglbmo  18584  tosso  18591  mgmplusf  18826  mgmn0plusgf  18827  ismgmd  18830  grpinva  18855  imasmgm2  18863  qusmgm  18864  idmgmhm  18890  resmgmhm  18900  resmgmhm2  18901  resmgmhm2b  18902  mgmhmco  18903  mgmhmima  18904  submgmacs  18906  sgrpidmnd  18928  ismndd  18946  imasmnd2  18968  qusmnd  18975  idmhm  18990  mndvcl  18992  issubm2  18999  0mhm  19015  resmhm  19016  resmhm2  19017  resmhm2b  19018  mhmco  19019  mhmimalem  19020  submacs  19023  prdspjmhm  19025  pwsdiagmhm  19027  pwsco1mhm  19028  pwsco2mhm  19029  gsumwsubmcl  19033  gsumsgrpccat  19036  gsumwmhm  19041  grpinvcnv  19217  grpinvnzcl  19221  grpsubf  19229  imasgrp2  19265  qusgrp2  19268  mhmfmhm  19275  mulgnnsubcl  19296  mulgnndir  19313  issubg4  19356  isnsg3  19370  nsgacs  19372  nsgid  19380  qusadd  19403  qus0subgadd  19414  ghmmhm  19440  ghmmhmb  19441  idghm  19445  resghm  19446  ghmf1  19460  qusghm  19469  gaid  19513  subgga  19514  gasubg  19516  invoppggim  19574  gsmsymgrfix  19642  smndlsmidm  19870  pj1ghm  19917  mulgnn0di  20039  mulgmhm  20041  mulgghm  20042  ghmfghm  20044  invghm  20047  ghmplusg  20060  ablnsg  20061  qusabl  20079  gsumval3eu  20118  gsumval3  20121  gsumzcl2  20124  gsumzaddlem  20135  gsumzadd  20136  gsumzmhm  20151  gsumzoppg  20158  srgfcl  20422  srgcom4lem  20439  srgmulgass  20443  srglmhm  20447  srgrmhm  20448  ringcomlem  20508  ringlghm  20543  ringrghm  20544  pwspjmhmmgpd  20557  c0mgm  20689  c0mhm  20690  isnzr2  20768  subrngringnsg  20805  issubrng2  20810  rhmimasubrnglem  20817  issubrg2  20844  domnmuln0  20961  isdomn3  20966  isdrng3lem2  21006  issrngd  21112  islmodd  21141  lmodscaf  21159  lcomf  21176  lmodvsghm  21198  rmodislmodlem  21204  lssacs  21242  idlmhm  21316  invlmhm  21317  lmhmvsca  21320  reslmhm2  21328  reslmhm2b  21329  pwsdiaglmhm  21332  pwssplit2  21335  pwssplit3  21336  issubrgd  21464  qusrhm  21570  qusmul2idl  21574  crngridl  21575  qusmulrng  21578  cmprmidlmcl  21631  expmhm  21742  zntoslem  21862  znfld  21866  psgnghm  21886  phlipf  21958  frlmup1  22104  asclghm  22190  asclrhm  22198  rnasclmulcl  22202  psraddcl  22247  psrvscacl  22259  psrass23  22276  psrbagev1  22386  coe1sclmulfv  22602  cply1mul  22614  evls1fpws  22687  rhmply1vsca  22703  matbas2d  22738  submaeval  22897  minmar1eval  22964  cpmatacl  23034  pmatcollpw1  23094  pmatcollpw  23099  tgclb  23288  topbas  23290  ntrss  23373  mretopd  23410  neissex  23445  cnpnei  23582  lmcnp  23622  ordthaus  23702  llynlly  23796  restnlly  23801  llyidm  23807  nllyidm  23808  ptbasin  23896  txcnp  23939  ist0-4  24048  kqt0lem  24055  isr0  24056  regr1lem2  24059  cmphmph  24107  connhmph  24108  fbun  24159  trfbas2  24162  isfil2  24175  isfild  24177  infil  24182  fbasfip  24187  fbasrn  24203  trfil2  24206  rnelfmlem  24271  fmfnfmlem3  24275  flimopn  24294  txflf  24325  fclsnei  24338  fclsfnflim  24346  fcfnei  24354  clssubg  24428  tgphaus  24436  qustgplem  24440  tsmsadd  24466  psmetxrge0  24632  psmetlecl  24634  xmetlecl  24665  xmettpos  24668  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  elbl3ps  24710  elbl3  24711  metss  24827  comet  24832  stdbdxmet  24834  stdbdmet  24835  methaus  24839  nrmmetd  24893  abvmet  24894  isngp4  24931  subgngp  24954  nmoi2  25049  nmoleub  25050  nmoid  25061  bl2ioo  25111  zcld  25133  divcn  25189  divccn  25194  cncfcdm  25219  divccncf  25227  icoopnst  25260  clmzlmvsca  25434  cph2ass  25534  tcphcph  25558  cfilfcls  25595  bcthlem2  25646  rrxmet  25729  rrxdstprj1  25730  rrxdsfi  25732  cldcss  25762  dvrec  26275  dvmptfsum  26295  aalioulem3  26661  taylply2  26695  efsubm  26879  dchrelbasd  27566  dchrmulcl  27576  2sqreulem3  27780  pntrmax  27891  padicabv  27957  nosupbnd2  28073  noinfbnd2  28088  sltsd  28154  divmulsw  28579  axtgcont  28931  xmstrkgc  29463  axsegconlem1  29495  axlowdimlem15  29534  usgredg2vlem1  29806  usgredg2vlem2  29807  iswlkon  30236  wwlksnextsurj  30489  elwwlks2  30558  elwspths2spth  30559  frrusgrord  30942  numclwwlk1lem2foalem  30952  grpoidinvlem2  31107  grpoidinvlem3  31108  ablo4  31152  ablomuldiv  31154  nvaddsub4  31259  nvmeq0  31260  sspmval  31335  sspimsval  31340  lnosub  31361  dipsubdir  31450  hvadd4  31638  hvpncan  31641  his35  31690  hiassdi  31693  shscli  31919  shmodsi  31991  chj4  32137  spansnmul  32166  spansncol  32170  spanunsni  32181  hoadd4  32386  hosubadd4  32416  lnopl  32516  unopf1o  32518  counop  32523  lnfnl  32533  hmopadj2  32543  eighmre  32565  lnopmi  32602  lnophsi  32603  hmops  32622  hmopm  32623  cnlnadjlem2  32670  adjmul  32694  adjadd  32695  kbass6  32723  mdslj1i  32921  mdslj2i  32922  mdslmd1lem1  32927  mdslmd2i  32932  chirredlem3  32994  isoun  33295  xdivmul  33491  odutos  33529  lmodvslmhm  33611  isarchi2  33746  archiabllem2  33758  imasmhm  33915  imasghm  33916  imasrhm  33917  imaslmhm  33918  quslmhm  33920  tngdim  34245  fedgmullem2  34262  metider  34526  pl1cn  34587  rossros  34813  ismeas  34832  dya2iocnei  34914  inelcarsg  34943  signstfvc  35203  bnj563  35374  fisshasheq  35903  cnpconn  35995  cvmseu  36041  elmrsubrn  36285  mrsubco  36286  fneint  37136  fnessref  37145  tailfb  37165  onsucuni3  38290  pibt2  38340  ptrecube  38538  poimirlem4  38542  heicant  38573  mblfinlem1  38575  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  cnambfre  38586  itg2addnclem2  38590  ftc1anclem5  38615  ftc1anclem6  38616  metf1o  38689  isbnd3b  38719  equivbnd  38724  heiborlem3  38747  rrnmet  38763  rrndstprj1  38764  rrntotbnd  38770  exidcl  38810  ghomco  38825  ghomdiv  38826  grpokerinj  38827  rngoneglmul  38877  rngonegrmul  38878  rngosubdi  38879  rngosubdir  38880  isdrngo2  38892  rngohomco  38908  rngoisocnv  38915  riscer  38922  crngm4  38937  crngohomfo  38940  idlsubcl  38957  inidl  38964  keridl  38966  ispridlc  39004  pridlc3  39007  dmncan1  39010  lflvscl  40134  3dim0  40514  linepsubN  40809  cdlemg2fvlem  41651  trlcoat  41780  istendod  41819  dva1dim  42042  dvhvaddcomN  42153  dihf11  42324  dihlatat  42394  sn-sup2  43555  fsuppssind  43621  mhphf  43625  ismrc  43711  isnacs3  43720  mzpindd  43756  pellex  43841  monotoddzzfi  43948  lermxnn0  43956  rmyeq0  43959  rmyeq  43960  lermy  43961  jm2.27  44014  lsmfgcl  44075  fsumcnsrcl  44167  rngunsnply  44170  gsumws3  45195  mnringmulrcld  45225  nzin  45301  ofdivrec  45309  ofdivcan4  45310  chordthmALT  45914  wessf1ornlem  46199  projf1o  46210  ltdiv23neg  46404  fmulcl  46592  prproropf1olem2  48585  prproropf1olem4  48587  mgmplusgiopALT  49290  idomcanl  49443  itsclc0xyqsolb  49881  toslat  50089  cicerALT  50153