Theorem 3expb 1266

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3adant3r1  1274  3adant3r2  1275  3adant3r3  1276  3adant1l  1318  3adant1r  1319  mp3an1  1411  sotri  5523  fnfco  6069  mpt2eq3dva  6719  oprres  6802  fovrnda  6805  grprinvd  6873  fnmpt2ovd  7252  offval22  7253  bropfvvvvlem  7256  fnsuppres  7322  suppsssn  7330  sprmpt2d  7350  oaass  7641  omlimcl  7658  odi  7659  nnmsucr  7705  cflim2  9085  mulcanenq  9782  mul4  10205  add4  10256  2addsub  10295  addsubeq4  10296  subadd4  10325  muladd  10462  ltleadd  10511  divmul  10688  divne0  10697  div23  10704  div12  10707  divsubdir  10721  divcan5  10727  divmuleq  10730  divcan6  10732  divdiv32  10733  div2sub  10850  letrp1  10865  lemul12b  10880  lediv1  10888  lt2mul2div  10901  lemuldiv  10903  ltdiv2  10909  ledivdiv  10912  lediv2  10913  ltdiv23  10914  lediv23  10915  sup2  10979  cju  11016  nndivre  11056  nndivtr  11062  nn0addge1  11339  nn0addge2  11340  peano2uz2  11465  uzind  11469  uzind3  11471  fzind  11475  fnn0ind  11476  uzind4  11746  qre  11793  irrmul  11813  rpdivcl  11856  rerpdivcl  11861  xrinfmsslem  12138  ixxin  12192  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzaddel  12375  fzadd2  12376  fzrev  12403  modlt  12679  modcyc  12705  axdc4uzlem  12782  expdiv  12911  fundmge2nop0  13274  swrd00  13418  swrdcl  13419  swrd0  13434  swrdccat  13493  swrdco  13583  2shfti  13820  isermulc2  14388  fsummulc2  14516  dvdscmulr  15010  dvdsmulcr  15011  dvds2add  15015  dvds2sub  15016  dvdstr  15018  alzdvds  15042  divalg2  15128  dvdslegcd  15226  lcmgcdlem  15319  lcmgcdeq  15325  isprm6  15426  pcqcl  15561  vdwmc2  15683  ressinbas  15936  cicer  16466  isposd  16955  pleval2i  16964  tosso  17036  poslubmo  17146  posglbmo  17147  mgmplusf  17251  ismndd  17313  imasmnd2  17327  idmhm  17344  issubm2  17348  0mhm  17358  resmhm  17359  resmhm2  17360  resmhm2b  17361  mhmco  17362  mhmima  17363  submacs  17365  prdspjmhm  17367  pwsdiagmhm  17369  pwsco1mhm  17370  pwsco2mhm  17371  gsumwsubmcl  17375  gsumccat  17378  gsumwmhm  17382  grpinvcnv  17483  grpinvnzcl  17487  grpsubf  17494  imasgrp2  17530  qusgrp2  17533  mhmfmhm  17538  mulgnnsubcl  17553  mulgnndir  17569  mulgnndirOLD  17570  issubg4  17613  isnsg3  17628  nsgacs  17630  nsgid  17640  qusadd  17651  ghmmhm  17670  ghmmhmb  17671  idghm  17675  resghm  17676  ghmf1  17689  qusghm  17697  gaid  17732  subgga  17733  gasubg  17735  invoppggim  17790  gsmsymgrfix  17848  lsmidm  18077  pj1ghm  18116  mulgnn0di  18231  mulgmhm  18233  mulgghm  18234  ghmfghm  18236  invghm  18239  ghmplusg  18249  ablnsg  18250  qusabl  18268  gsumval3eu  18305  gsumval3  18308  gsumzcl2  18311  gsumzaddlem  18321  gsumzadd  18322  gsumzmhm  18337  gsumzoppg  18344  srgfcl  18515  srgmulgass  18531  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  issubrg2  18800  issrngd  18861  islmodd  18869  lmodscaf  18885  lcomf  18902  lmodvsghm  18924  rmodislmodlem  18930  lssacs  18967  idlmhm  19041  invlmhm  19042  lmhmvsca  19045  reslmhm2  19053  reslmhm2b  19054  pwsdiaglmhm  19057  pwssplit2  19060  pwssplit3  19061  issubrngd2  19189  qusrhm  19237  crngridl  19238  quscrng  19240  isnzr2  19263  domnmuln0  19298  opprdomn  19301  asclghm  19338  asclrhm  19342  psraddcl  19383  psrvscacl  19393  psrass23  19410  psrbagev1  19510  coe1sclmulfv  19653  cply1mul  19664  expmhm  19815  zntoslem  19905  znfld  19909  psgnghm  19926  phlipf  19997  frlmup1  20137  mndvcl  20197  matbas2d  20229  submaeval  20388  minmar1eval  20455  cpmatacl  20521  pmatcollpw1  20581  pmatcollpw  20586  tgclb  20774  topbas  20776  ntrss  20859  mretopd  20896  neissex  20931  cnpnei  21068  lmcnp  21108  ordthaus  21188  llynlly  21280  restnlly  21285  llyidm  21291  nllyidm  21292  ptbasin  21380  txcnp  21423  ist0-4  21532  kqt0lem  21539  isr0  21540  regr1lem2  21543  cmphmph  21591  connhmph  21592  fbun  21644  trfbas2  21647  isfil2  21660  isfild  21662  infil  21667  fbasfip  21672  fbasrn  21688  trfil2  21691  rnelfmlem  21756  fmfnfmlem3  21760  flimopn  21779  txflf  21810  fclsnei  21823  fclsfnflim  21831  fcfnei  21839  clssubg  21912  tgphaus  21920  qustgplem  21924  tsmsadd  21950  psmetxrge0  22118  psmetlecl  22120  xmetlecl  22151  xmettpos  22154  imasdsf1olem  22178  imasf1oxmet  22180  imasf1omet  22181  elbl3ps  22196  elbl3  22197  metss  22313  comet  22318  stdbdxmet  22320  stdbdmet  22321  methaus  22325  nrmmetd  22379  abvmet  22380  isngp4  22416  subgngp  22439  nmoi2  22534  nmoleub  22535  nmoid  22546  bl2ioo  22595  zcld  22616  divcn  22671  divccn  22676  cncffvrn  22701  divccncf  22709  icoopnst  22738  clmzlmvsca  22913  cph2ass  23013  tchcph  23036  cfilfcls  23072  bcthlem2  23122  rrxmet  23191  rrxdstprj1  23192  cldcss  23212  dvrec  23718  dvmptfsum  23738  aalioulem3  24089  taylply2  24122  efsubm  24297  dchrelbasd  24964  dchrmulcl  24974  pntrmax  25253  padicabv  25319  axtgcont  25368  xmstrkgc  25766  axsegconlem1  25797  axlowdimlem15  25836  usgredg2vlem1  26117  usgredg2vlem2  26118  iswlkon  26553  wlknwwlksninj  26775  wwlksnextsur  26795  elwwlks2  26861  elwspths2spth  26862  frgr2wwlk1  27193  frrusgrord  27205  numclwlk1lem2foalem  27222  grpoidinvlem2  27359  grpoidinvlem3  27360  ablo4  27404  ablomuldiv  27406  nvaddsub4  27512  nvmeq0  27513  sspmval  27588  sspimsval  27593  lnosub  27614  dipsubdir  27703  sspph  27710  hvadd4  27893  hvpncan  27896  his35  27945  hiassdi  27948  shscli  28176  shmodsi  28248  chj4  28394  spansnmul  28423  spansncol  28427  spanunsni  28438  hoadd4  28643  hosubadd4  28673  lnopl  28773  unopf1o  28775  counop  28780  lnfnl  28790  hmopadj2  28800  eighmre  28822  lnopmi  28859  lnophsi  28860  hmops  28879  hmopm  28880  cnlnadjlem2  28927  adjmul  28951  adjadd  28952  kbass6  28980  mdslj1i  29178  mdslj2i  29179  mdslmd1lem1  29184  mdslmd2i  29189  chirredlem3  29251  isoun  29479  xdivmul  29633  odutos  29663  isarchi2  29739  archiabllem2  29751  metider  29937  pl1cn  30001  rossros  30243  ismeas  30262  dya2iocnei  30344  inelcarsg  30373  bnj563  30813  cnpconn  31212  cvmseu  31258  elmrsubrn  31417  mrsubco  31418  subdivcomb1  31611  nosupbnd2  31862  fneint  32343  fnessref  32352  tailfb  32372  onsucuni3  33215  ptrecube  33409  poimirlem4  33413  heicant  33444  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  cnambfre  33458  itg2addnclem2  33462  ftc1anclem5  33489  ftc1anclem6  33490  metf1o  33551  isbnd3b  33584  equivbnd  33589  heiborlem3  33612  rrnmet  33628  rrndstprj1  33629  rrntotbnd  33635  exidcl  33675  ghomco  33690  ghomdiv  33691  grpokerinj  33692  rngoneglmul  33742  rngonegrmul  33743  rngosubdi  33744  rngosubdir  33745  isdrngo2  33757  rngohomco  33773  rngoisocnv  33780  riscer  33787  crngm4  33802  crngohomfo  33805  idlsubcl  33822  inidl  33829  keridl  33831  ispridlc  33869  pridlc3  33872  dmncan1  33875  lflvscl  34364  3dim0  34743  linepsubN  35038  cdlemg2fvlem  35882  trlcoat  36011  istendod  36050  dva1dim  36273  dvhvaddcomN  36385  dihf11  36556  dihlatat  36626  ismrc  37264  isnacs3  37273  mzpindd  37309  pellex  37399  monotoddzzfi  37507  lermxnn0  37517  rmyeq0  37520  rmyeq  37521  lermy  37522  jm2.27  37575  lsmfgcl  37644  fsumcnsrcl  37736  rngunsnply  37743  isdomn3  37782  gsumws3  38499  nzin  38517  ofdivrec  38525  ofdivcan4  38526  chordthmALT  39169  projf1o  39386  ltdiv23neg  39617  fmulcl  39813  rrxdsfi  40505  ismgmd  41776  idmgmhm  41788  resmgmhm  41798  resmgmhm2  41799  resmgmhm2b  41800  mgmhmco  41801  mgmhmima  41802  submgmacs  41804  mgmplusgiopALT  41830  c0mgm  41909  c0mhm  41910