Theorem 3expb 1120

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 1119	. 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  1121  3adant3r1  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1450  sotri  6084  fnfco  6699  mpoeq3dva  7435  oprres  7526  fovcdmda  7529  fnmpoovd  8029  offval22  8030  bropfvvvvlem  8033  fnsuppres  8133  suppsssn  8143  sprmpod  8166  oaass  8488  omlimcl  8505  odi  8506  nnmsucr  8553  nnasmo  8591  unfi  9097  ttrclse  9638  cflim2  10175  mulcanenq  10873  mul4  11303  add4  11356  2addsub  11396  addsubeq4  11397  subadd4  11427  muladd  11571  ltleadd  11622  divmul  11801  divne0  11810  div23  11817  div12  11820  div11  11826  divsubdir  11837  subdivcomb1  11838  divcan5  11845  divmuleq  11848  divcan6  11850  divdiv32  11851  div2sub  11968  letrp1  11987  lemul12b  12000  lediv1  12009  lt2mul2div  12022  lemuldiv  12024  ltdiv2  12030  ledivdiv  12033  lediv2  12034  ltdiv23  12035  lediv23  12036  sup2  12100  cju  12143  nndivre  12188  nndivtr  12194  nn0addge1  12449  nn0addge2  12450  peano2uz2  12582  uzind  12586  uzind3  12588  fzind  12592  fnn0ind  12593  uzind4  12821  qre  12868  irrmul  12889  rpdivcl  12934  rerpdivcl  12939  xrinfmsslem  13225  ixxin  13280  iccshftr  13404  iccshftl  13406  iccdil  13408  icccntr  13410  fzaddel  13476  fzadd2  13477  fzrev  13505  modlt  13802  modcyc  13828  axdc4uzlem  13908  expdiv  14038  fundmge2nop0  14427  swrd00  14570  swrdcl  14571  swrdnnn0nd  14582  swrd0  14584  swrdwrdsymb  14588  ccatpfx  14626  swrdccat  14660  splid  14678  swrdco  14762  2shfti  15005  isermulc2  15583  fsummulc2  15709  dvdscmulr  16213  dvdsmulcr  16214  dvds2add  16219  dvds2sub  16220  dvdstr  16223  alzdvds  16249  divalg2  16334  dvdslegcd  16433  lcmgcdlem  16535  lcmgcdeq  16541  isprm6  16643  pcqcl  16786  vdwmc2  16909  ressinbas  17174  cicer  17732  isposd  18247  pleval2i  18259  poslubmo  18334  posglbmo  18335  tosso  18342  mgmplusf  18577  ismgmd  18579  grpinva  18601  idmgmhm  18628  resmgmhm  18638  resmgmhm2  18639  resmgmhm2b  18640  mgmhmco  18641  mgmhmima  18642  submgmacs  18644  sgrpidmnd  18666  ismndd  18683  imasmnd2  18701  idmhm  18722  mndvcl  18724  issubm2  18731  0mhm  18746  resmhm  18747  resmhm2  18748  resmhm2b  18749  mhmco  18750  mhmimalem  18751  submacs  18754  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  grpinvcnv  18938  grpinvnzcl  18943  grpsubf  18951  imasgrp2  18987  qusgrp2  18990  mhmfmhm  18997  mulgnnsubcl  19018  mulgnndir  19035  issubg4  19077  isnsg3  19091  nsgacs  19093  nsgid  19101  qusadd  19119  qus0subgadd  19130  ghmmhm  19157  ghmmhmb  19158  idghm  19162  resghm  19163  ghmf1  19177  qusghm  19186  gaid  19230  subgga  19231  gasubg  19233  invoppggim  19291  gsmsymgrfix  19359  smndlsmidm  19587  pj1ghm  19634  mulgnn0di  19756  mulgmhm  19758  mulgghm  19759  ghmfghm  19761  invghm  19764  ghmplusg  19777  ablnsg  19778  qusabl  19796  gsumval3eu  19835  gsumval3  19838  gsumzcl2  19841  gsumzaddlem  19852  gsumzadd  19853  gsumzmhm  19868  gsumzoppg  19875  srgfcl  20133  srgcom4lem  20150  srgmulgass  20154  srglmhm  20158  srgrmhm  20159  ringcomlem  20216  ringlghm  20249  ringrghm  20250  pwspjmhmmgpd  20265  c0mgm  20397  c0mhm  20398  isnzr2  20453  subrngringnsg  20488  issubrng2  20493  rhmimasubrnglem  20500  issubrg2  20527  domnmuln0  20644  isdomn3  20650  issrngd  20790  islmodd  20819  lmodscaf  20837  lcomf  20854  lmodvsghm  20876  rmodislmodlem  20882  lssacs  20920  idlmhm  20995  invlmhm  20996  lmhmvsca  20999  reslmhm2  21007  reslmhm2b  21008  pwsdiaglmhm  21011  pwssplit2  21014  pwssplit3  21015  issubrgd  21143  qusrhm  21233  qusmul2idl  21236  crngridl  21237  qusmulrng  21239  expmhm  21393  zntoslem  21513  znfld  21517  psgnghm  21537  phlipf  21609  frlmup1  21755  asclghm  21840  asclrhm  21848  rnasclmulcl  21852  psraddcl  21896  psraddclOLD  21897  psrvscacl  21909  psrass23  21926  psrbagev1  22034  coe1sclmulfv  22227  cply1mul  22242  evls1fpws  22315  rhmply1vsca  22334  matbas2d  22369  submaeval  22528  minmar1eval  22595  cpmatacl  22662  pmatcollpw1  22722  pmatcollpw  22727  tgclb  22916  topbas  22918  ntrss  23001  mretopd  23038  neissex  23073  cnpnei  23210  lmcnp  23250  ordthaus  23330  llynlly  23423  restnlly  23428  llyidm  23434  nllyidm  23435  ptbasin  23523  txcnp  23566  ist0-4  23675  kqt0lem  23682  isr0  23683  regr1lem2  23686  cmphmph  23734  connhmph  23735  fbun  23786  trfbas2  23789  isfil2  23802  isfild  23804  infil  23809  fbasfip  23814  fbasrn  23830  trfil2  23833  rnelfmlem  23898  fmfnfmlem3  23902  flimopn  23921  txflf  23952  fclsnei  23965  fclsfnflim  23973  fcfnei  23981  clssubg  24055  tgphaus  24063  qustgplem  24067  tsmsadd  24093  psmetxrge0  24259  psmetlecl  24261  xmetlecl  24292  xmettpos  24295  imasdsf1olem  24319  imasf1oxmet  24321  imasf1omet  24322  elbl3ps  24337  elbl3  24338  metss  24454  comet  24459  stdbdxmet  24461  stdbdmet  24462  methaus  24466  nrmmetd  24520  abvmet  24521  isngp4  24558  subgngp  24581  nmoi2  24676  nmoleub  24677  nmoid  24688  bl2ioo  24738  zcld  24760  divcnOLD  24815  divcn  24817  divccn  24822  divccnOLD  24824  cncfcdm  24849  divccncf  24857  icoopnst  24894  clmzlmvsca  25071  cph2ass  25171  tcphcph  25195  cfilfcls  25232  bcthlem2  25283  rrxmet  25366  rrxdstprj1  25367  rrxdsfi  25369  cldcss  25399  dvrec  25917  dvmptfsum  25937  aalioulem3  26300  taylply2  26333  taylply2OLD  26334  efsubm  26518  dchrelbasd  27208  dchrmulcl  27218  2sqreulem3  27422  pntrmax  27533  padicabv  27599  nosupbnd2  27686  noinfbnd2  27701  sltsd  27766  divmulsw  28191  axtgcont  28543  xmstrkgc  28960  axsegconlem1  28992  axlowdimlem15  29031  usgredg2vlem1  29300  usgredg2vlem2  29301  iswlkon  29731  wwlksnextsurj  29975  elwwlks2  30044  elwspths2spth  30045  frrusgrord  30418  numclwwlk1lem2foalem  30428  grpoidinvlem2  30582  grpoidinvlem3  30583  ablo4  30627  ablomuldiv  30629  nvaddsub4  30734  nvmeq0  30735  sspmval  30810  sspimsval  30815  lnosub  30836  dipsubdir  30925  hvadd4  31113  hvpncan  31116  his35  31165  hiassdi  31168  shscli  31394  shmodsi  31466  chj4  31612  spansnmul  31641  spansncol  31645  spanunsni  31656  hoadd4  31861  hosubadd4  31891  lnopl  31991  unopf1o  31993  counop  31998  lnfnl  32008  hmopadj2  32018  eighmre  32040  lnopmi  32077  lnophsi  32078  hmops  32097  hmopm  32098  cnlnadjlem2  32145  adjmul  32169  adjadd  32170  kbass6  32198  mdslj1i  32396  mdslj2i  32397  mdslmd1lem1  32402  mdslmd2i  32407  chirredlem3  32469  isoun  32783  xdivmul  33008  odutos  33052  lmodvslmhm  33135  isarchi2  33269  archiabllem2  33281  imasmhm  33437  imasghm  33438  imasrhm  33439  imaslmhm  33440  quslmhm  33442  tngdim  33772  fedgmullem2  33789  metider  34053  pl1cn  34114  rossros  34339  ismeas  34358  dya2iocnei  34441  inelcarsg  34470  signstfvc  34733  bnj563  34901  fisshasheq  35311  cnpconn  35426  cvmseu  35472  elmrsubrn  35716  mrsubco  35717  fneint  36544  fnessref  36553  tailfb  36573  onsucuni3  37574  pibt2  37624  ptrecube  37823  poimirlem4  37827  heicant  37858  mblfinlem1  37860  mblfinlem2  37861  mblfinlem3  37862  mblfinlem4  37863  cnambfre  37871  itg2addnclem2  37875  ftc1anclem5  37900  ftc1anclem6  37901  metf1o  37958  isbnd3b  37988  equivbnd  37993  heiborlem3  38016  rrnmet  38032  rrndstprj1  38033  rrntotbnd  38039  exidcl  38079  ghomco  38094  ghomdiv  38095  grpokerinj  38096  rngoneglmul  38146  rngonegrmul  38147  rngosubdi  38148  rngosubdir  38149  isdrngo2  38161  rngohomco  38177  rngoisocnv  38184  riscer  38191  crngm4  38206  crngohomfo  38209  idlsubcl  38226  inidl  38233  keridl  38235  ispridlc  38273  pridlc3  38276  dmncan1  38279  lflvscl  39359  3dim0  39739  linepsubN  40034  cdlemg2fvlem  40876  trlcoat  41005  istendod  41044  dva1dim  41267  dvhvaddcomN  41378  dihf11  41549  dihlatat  41619  sn-sup2  42767  fsuppssind  42857  mhphf  42861  ismrc  42964  isnacs3  42973  mzpindd  43009  pellex  43098  monotoddzzfi  43205  lermxnn0  43213  rmyeq0  43216  rmyeq  43217  lermy  43218  jm2.27  43271  lsmfgcl  43337  fsumcnsrcl  43429  rngunsnply  43432  gsumws3  44458  mnringmulrcld  44490  nzin  44580  ofdivrec  44588  ofdivcan4  44589  chordthmALT  45194  wessf1ornlem  45450  projf1o  45462  ltdiv23neg  45659  fmulcl  45848  prproropf1olem2  47771  prproropf1olem4  47773  mgmplusgiopALT  48461  itsclc0xyqsolb  49037  toslat  49248  cicerALT  49312