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  6079  fnfco  6694  mpoeq3dva  7429  oprres  7520  fovcdmda  7523  fnmpoovd  8023  offval22  8024  bropfvvvvlem  8027  fnsuppres  8127  suppsssn  8137  sprmpod  8160  oaass  8482  omlimcl  8499  odi  8500  nnmsucr  8546  nnasmo  8584  unfi  9086  ttrclse  9623  cflim2  10160  mulcanenq  10857  mul4  11287  add4  11340  2addsub  11380  addsubeq4  11381  subadd4  11411  muladd  11555  ltleadd  11606  divmul  11785  divne0  11794  div23  11801  div12  11804  div11  11810  divsubdir  11821  subdivcomb1  11822  divcan5  11829  divmuleq  11832  divcan6  11834  divdiv32  11835  div2sub  11952  letrp1  11971  lemul12b  11984  lediv1  11993  lt2mul2div  12006  lemuldiv  12008  ltdiv2  12014  ledivdiv  12017  lediv2  12018  ltdiv23  12019  lediv23  12020  sup2  12084  cju  12127  nndivre  12172  nndivtr  12178  nn0addge1  12433  nn0addge2  12434  peano2uz2  12567  uzind  12571  uzind3  12573  fzind  12577  fnn0ind  12578  uzind4  12810  qre  12857  irrmul  12878  rpdivcl  12923  rerpdivcl  12928  xrinfmsslem  13213  ixxin  13268  iccshftr  13392  iccshftl  13394  iccdil  13396  icccntr  13398  fzaddel  13464  fzadd2  13465  fzrev  13493  modlt  13790  modcyc  13816  axdc4uzlem  13896  expdiv  14026  fundmge2nop0  14415  swrd00  14558  swrdcl  14559  swrdnnn0nd  14570  swrd0  14572  swrdwrdsymb  14576  ccatpfx  14614  swrdccat  14648  splid  14666  swrdco  14750  2shfti  14993  isermulc2  15571  fsummulc2  15697  dvdscmulr  16201  dvdsmulcr  16202  dvds2add  16207  dvds2sub  16208  dvdstr  16211  alzdvds  16237  divalg2  16322  dvdslegcd  16421  lcmgcdlem  16523  lcmgcdeq  16529  isprm6  16631  pcqcl  16774  vdwmc2  16897  ressinbas  17162  cicer  17719  isposd  18234  pleval2i  18246  poslubmo  18321  posglbmo  18322  tosso  18329  mgmplusf  18564  ismgmd  18566  grpinva  18588  idmgmhm  18615  resmgmhm  18625  resmgmhm2  18626  resmgmhm2b  18627  mgmhmco  18628  mgmhmima  18629  submgmacs  18631  sgrpidmnd  18653  ismndd  18670  imasmnd2  18688  idmhm  18709  mndvcl  18711  issubm2  18718  0mhm  18733  resmhm  18734  resmhm2  18735  resmhm2b  18736  mhmco  18737  mhmimalem  18738  submacs  18741  prdspjmhm  18743  pwsdiagmhm  18745  pwsco1mhm  18746  pwsco2mhm  18747  gsumwsubmcl  18751  gsumsgrpccat  18754  gsumwmhm  18759  grpinvcnv  18925  grpinvnzcl  18930  grpsubf  18938  imasgrp2  18974  qusgrp2  18977  mhmfmhm  18984  mulgnnsubcl  19005  mulgnndir  19022  issubg4  19064  isnsg3  19078  nsgacs  19080  nsgid  19088  qusadd  19106  qus0subgadd  19117  ghmmhm  19144  ghmmhmb  19145  idghm  19149  resghm  19150  ghmf1  19164  qusghm  19173  gaid  19217  subgga  19218  gasubg  19220  invoppggim  19278  gsmsymgrfix  19346  smndlsmidm  19574  pj1ghm  19621  mulgnn0di  19743  mulgmhm  19745  mulgghm  19746  ghmfghm  19748  invghm  19751  ghmplusg  19764  ablnsg  19765  qusabl  19783  gsumval3eu  19822  gsumval3  19825  gsumzcl2  19828  gsumzaddlem  19839  gsumzadd  19840  gsumzmhm  19855  gsumzoppg  19862  srgfcl  20120  srgcom4lem  20137  srgmulgass  20141  srglmhm  20145  srgrmhm  20146  ringcomlem  20203  ringlghm  20236  ringrghm  20237  pwspjmhmmgpd  20252  c0mgm  20383  c0mhm  20384  isnzr2  20439  subrngringnsg  20474  issubrng2  20479  rhmimasubrnglem  20486  issubrg2  20513  domnmuln0  20630  isdomn3  20636  issrngd  20776  islmodd  20805  lmodscaf  20823  lcomf  20840  lmodvsghm  20862  rmodislmodlem  20868  lssacs  20906  idlmhm  20981  invlmhm  20982  lmhmvsca  20985  reslmhm2  20993  reslmhm2b  20994  pwsdiaglmhm  20997  pwssplit2  21000  pwssplit3  21001  issubrgd  21129  qusrhm  21219  qusmul2idl  21222  crngridl  21223  qusmulrng  21225  expmhm  21379  zntoslem  21499  znfld  21503  psgnghm  21523  phlipf  21595  frlmup1  21741  asclghm  21826  asclrhm  21833  rnasclmulcl  21837  psraddcl  21881  psraddclOLD  21882  psrvscacl  21894  psrass23  21912  psrbagev1  22018  coe1sclmulfv  22203  cply1mul  22217  evls1fpws  22290  rhmply1vsca  22309  matbas2d  22344  submaeval  22503  minmar1eval  22570  cpmatacl  22637  pmatcollpw1  22697  pmatcollpw  22702  tgclb  22891  topbas  22893  ntrss  22976  mretopd  23013  neissex  23048  cnpnei  23185  lmcnp  23225  ordthaus  23305  llynlly  23398  restnlly  23403  llyidm  23409  nllyidm  23410  ptbasin  23498  txcnp  23541  ist0-4  23650  kqt0lem  23657  isr0  23658  regr1lem2  23661  cmphmph  23709  connhmph  23710  fbun  23761  trfbas2  23764  isfil2  23777  isfild  23779  infil  23784  fbasfip  23789  fbasrn  23805  trfil2  23808  rnelfmlem  23873  fmfnfmlem3  23877  flimopn  23896  txflf  23927  fclsnei  23940  fclsfnflim  23948  fcfnei  23956  clssubg  24030  tgphaus  24038  qustgplem  24042  tsmsadd  24068  psmetxrge0  24234  psmetlecl  24236  xmetlecl  24267  xmettpos  24270  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  elbl3ps  24312  elbl3  24313  metss  24429  comet  24434  stdbdxmet  24436  stdbdmet  24437  methaus  24441  nrmmetd  24495  abvmet  24496  isngp4  24533  subgngp  24556  nmoi2  24651  nmoleub  24652  nmoid  24663  bl2ioo  24713  zcld  24735  divcnOLD  24790  divcn  24792  divccn  24797  divccnOLD  24799  cncfcdm  24824  divccncf  24832  icoopnst  24869  clmzlmvsca  25046  cph2ass  25146  tcphcph  25170  cfilfcls  25207  bcthlem2  25258  rrxmet  25341  rrxdstprj1  25342  rrxdsfi  25344  cldcss  25374  dvrec  25892  dvmptfsum  25912  aalioulem3  26275  taylply2  26308  taylply2OLD  26309  efsubm  26493  dchrelbasd  27183  dchrmulcl  27193  2sqreulem3  27397  pntrmax  27508  padicabv  27574  nosupbnd2  27661  noinfbnd2  27676  ssltd  27737  divsmulw  28138  axtgcont  28453  xmstrkgc  28870  axsegconlem1  28902  axlowdimlem15  28941  usgredg2vlem1  29210  usgredg2vlem2  29211  iswlkon  29641  wwlksnextsurj  29885  elwwlks2  29954  elwspths2spth  29955  frrusgrord  30328  numclwwlk1lem2foalem  30338  grpoidinvlem2  30492  grpoidinvlem3  30493  ablo4  30537  ablomuldiv  30539  nvaddsub4  30644  nvmeq0  30645  sspmval  30720  sspimsval  30725  lnosub  30746  dipsubdir  30835  hvadd4  31023  hvpncan  31026  his35  31075  hiassdi  31078  shscli  31304  shmodsi  31376  chj4  31522  spansnmul  31551  spansncol  31555  spanunsni  31566  hoadd4  31771  hosubadd4  31801  lnopl  31901  unopf1o  31903  counop  31908  lnfnl  31918  hmopadj2  31928  eighmre  31950  lnopmi  31987  lnophsi  31988  hmops  32007  hmopm  32008  cnlnadjlem2  32055  adjmul  32079  adjadd  32080  kbass6  32108  mdslj1i  32306  mdslj2i  32307  mdslmd1lem1  32312  mdslmd2i  32317  chirredlem3  32379  isoun  32690  xdivmul  32912  odutos  32956  lmodvslmhm  33037  isarchi2  33161  archiabllem2  33173  imasmhm  33326  imasghm  33327  imasrhm  33328  imaslmhm  33329  quslmhm  33331  tngdim  33633  fedgmullem2  33650  metider  33914  pl1cn  33975  rossros  34200  ismeas  34219  dya2iocnei  34302  inelcarsg  34331  signstfvc  34594  bnj563  34762  fisshasheq  35166  cnpconn  35281  cvmseu  35327  elmrsubrn  35571  mrsubco  35572  fneint  36399  fnessref  36408  tailfb  36428  onsucuni3  37418  pibt2  37468  ptrecube  37666  poimirlem4  37670  heicant  37701  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  cnambfre  37714  itg2addnclem2  37718  ftc1anclem5  37743  ftc1anclem6  37744  metf1o  37801  isbnd3b  37831  equivbnd  37836  heiborlem3  37859  rrnmet  37875  rrndstprj1  37876  rrntotbnd  37882  exidcl  37922  ghomco  37937  ghomdiv  37938  grpokerinj  37939  rngoneglmul  37989  rngonegrmul  37990  rngosubdi  37991  rngosubdir  37992  isdrngo2  38004  rngohomco  38020  rngoisocnv  38027  riscer  38034  crngm4  38049  crngohomfo  38052  idlsubcl  38069  inidl  38076  keridl  38078  ispridlc  38116  pridlc3  38119  dmncan1  38122  lflvscl  39182  3dim0  39562  linepsubN  39857  cdlemg2fvlem  40699  trlcoat  40828  istendod  40867  dva1dim  41090  dvhvaddcomN  41201  dihf11  41372  dihlatat  41442  sn-sup2  42590  fsuppssind  42692  mhphf  42696  ismrc  42799  isnacs3  42808  mzpindd  42844  pellex  42933  monotoddzzfi  43040  lermxnn0  43048  rmyeq0  43051  rmyeq  43052  lermy  43053  jm2.27  43106  lsmfgcl  43172  fsumcnsrcl  43264  rngunsnply  43267  gsumws3  44294  mnringmulrcld  44326  nzin  44416  ofdivrec  44424  ofdivcan4  44425  chordthmALT  45030  wessf1ornlem  45287  projf1o  45299  ltdiv23neg  45497  fmulcl  45686  prproropf1olem2  47609  prproropf1olem4  47611  mgmplusgiopALT  48299  itsclc0xyqsolb  48876  toslat  49087  cicerALT  49152