MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expb Structured version   Visualization version   GIF version

Theorem 3expb 1113
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
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1112 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 448 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  3expia  1114  3adant1lOLD  1167  3adant1rOLD  1169  3adant3r1  1174  3adant3r2  1175  3adant3r3  1176  mp3an1  1548  sotri  5669  fnfco  6218  mpt2eq3dva  6872  oprres  6955  fovrnda  6958  grprinvd  7026  fnmpt2ovd  7408  offval22  7409  bropfvvvvlem  7412  fnsuppres  7479  suppsssn  7487  sprmpt2d  7507  oaass  7798  omlimcl  7815  odi  7816  nnmsucr  7862  cflim2  9248  mulcanenq  9945  mul4  10368  add4  10419  2addsub  10458  addsubeq4  10459  subadd4  10488  muladd  10625  ltleadd  10674  divmul  10851  divne0  10860  div23  10867  div12  10870  divsubdir  10884  divcan5  10890  divmuleq  10893  divcan6  10895  divdiv32  10896  div2sub  11013  letrp1  11028  lemul12b  11043  lediv1  11051  lt2mul2div  11064  lemuldiv  11066  ltdiv2  11072  ledivdiv  11075  lediv2  11076  ltdiv23  11077  lediv23  11078  sup2  11142  cju  11179  nndivre  11219  nndivtr  11225  nn0addge1  11502  nn0addge2  11503  peano2uz2  11628  uzind  11632  uzind3  11634  fzind  11638  fnn0ind  11639  uzind4  11910  qre  11957  irrmul  11977  rpdivcl  12020  rerpdivcl  12025  xrinfmsslem  12302  ixxin  12356  iccshftr  12470  iccshftl  12472  iccdil  12474  icccntr  12476  fzaddel  12539  fzadd2  12540  fzrev  12567  modlt  12844  modcyc  12870  axdc4uzlem  12947  expdiv  13076  fundmge2nop0  13437  swrd00  13588  swrdcl  13589  swrd0  13605  swrdccat  13664  swrdco  13754  2shfti  13990  isermulc2  14558  fsummulc2  14686  dvdscmulr  15183  dvdsmulcr  15184  dvds2add  15188  dvds2sub  15189  dvdstr  15191  alzdvds  15215  divalg2  15301  dvdslegcd  15399  lcmgcdlem  15492  lcmgcdeq  15498  isprm6  15599  pcqcl  15734  vdwmc2  15856  ressinbas  16109  cicer  16638  isposd  17127  pleval2i  17136  tosso  17208  poslubmo  17318  posglbmo  17319  mgmplusf  17423  ismndd  17485  imasmnd2  17499  idmhm  17516  issubm2  17520  0mhm  17530  resmhm  17531  resmhm2  17532  resmhm2b  17533  mhmco  17534  mhmima  17535  submacs  17537  prdspjmhm  17539  pwsdiagmhm  17541  pwsco1mhm  17542  pwsco2mhm  17543  gsumwsubmcl  17547  gsumccat  17550  gsumwmhm  17554  grpinvcnv  17655  grpinvnzcl  17659  grpsubf  17666  imasgrp2  17702  qusgrp2  17705  mhmfmhm  17710  mulgnnsubcl  17725  mulgnndir  17741  mulgnndirOLD  17742  issubg4  17785  isnsg3  17800  nsgacs  17802  nsgid  17812  qusadd  17823  ghmmhm  17842  ghmmhmb  17843  idghm  17847  resghm  17848  ghmf1  17861  qusghm  17869  gaid  17903  subgga  17904  gasubg  17906  invoppggim  17961  gsmsymgrfix  18019  lsmidm  18248  pj1ghm  18287  mulgnn0di  18402  mulgmhm  18404  mulgghm  18405  ghmfghm  18407  invghm  18410  ghmplusg  18420  ablnsg  18421  qusabl  18439  gsumval3eu  18476  gsumval3  18479  gsumzcl2  18482  gsumzaddlem  18492  gsumzadd  18493  gsumzmhm  18508  gsumzoppg  18515  srgfcl  18686  srgmulgass  18702  srglmhm  18706  srgrmhm  18707  ringlghm  18775  ringrghm  18776  issubrg2  18973  issrngd  19034  islmodd  19042  lmodscaf  19058  lcomf  19075  lmodvsghm  19097  rmodislmodlem  19103  lssacs  19140  idlmhm  19214  invlmhm  19215  lmhmvsca  19218  reslmhm2  19226  reslmhm2b  19227  pwsdiaglmhm  19230  pwssplit2  19233  pwssplit3  19234  issubrngd2  19362  qusrhm  19410  crngridl  19411  quscrng  19413  isnzr2  19436  domnmuln0  19471  opprdomn  19474  asclghm  19511  asclrhm  19515  psraddcl  19556  psrvscacl  19566  psrass23  19583  psrbagev1  19683  coe1sclmulfv  19826  cply1mul  19837  expmhm  19988  zntoslem  20078  znfld  20082  psgnghm  20099  phlipf  20170  frlmup1  20310  mndvcl  20370  matbas2d  20402  submaeval  20561  minmar1eval  20628  cpmatacl  20694  pmatcollpw1  20754  pmatcollpw  20759  tgclb  20947  topbas  20949  ntrss  21032  mretopd  21069  neissex  21104  cnpnei  21241  lmcnp  21281  ordthaus  21361  llynlly  21453  restnlly  21458  llyidm  21464  nllyidm  21465  ptbasin  21553  txcnp  21596  ist0-4  21705  kqt0lem  21712  isr0  21713  regr1lem2  21716  cmphmph  21764  connhmph  21765  fbun  21816  trfbas2  21819  isfil2  21832  isfild  21834  infil  21839  fbasfip  21844  fbasrn  21860  trfil2  21863  rnelfmlem  21928  fmfnfmlem3  21932  flimopn  21951  txflf  21982  fclsnei  21995  fclsfnflim  22003  fcfnei  22011  clssubg  22084  tgphaus  22092  qustgplem  22096  tsmsadd  22122  psmetxrge0  22290  psmetlecl  22292  xmetlecl  22323  xmettpos  22326  imasdsf1olem  22350  imasf1oxmet  22352  imasf1omet  22353  elbl3ps  22368  elbl3  22369  metss  22485  comet  22490  stdbdxmet  22492  stdbdmet  22493  methaus  22497  nrmmetd  22551  abvmet  22552  isngp4  22588  subgngp  22611  nmoi2  22706  nmoleub  22707  nmoid  22718  bl2ioo  22767  zcld  22788  divcn  22843  divccn  22848  cncffvrn  22873  divccncf  22881  icoopnst  22910  clmzlmvsca  23084  cph2ass  23184  tchcph  23207  cfilfcls  23243  bcthlem2  23293  rrxmet  23362  rrxdstprj1  23363  cldcss  23383  dvrec  23888  dvmptfsum  23908  aalioulem3  24259  taylply2  24292  efsubm  24467  dchrelbasd  25134  dchrmulcl  25144  pntrmax  25423  padicabv  25489  axtgcont  25538  xmstrkgc  25936  axsegconlem1  25967  axlowdimlem15  26006  usgredg2vlem1  26287  usgredg2vlem2  26288  iswlkon  26734  wlknwwlksninj  26969  wwlksnextsur  26989  elwwlks2  27059  elwspths2spth  27060  frrusgrord  27466  numclwlk1lem2foalem  27481  grpoidinvlem2  27639  grpoidinvlem3  27640  ablo4  27684  ablomuldiv  27686  nvaddsub4  27792  nvmeq0  27793  sspmval  27868  sspimsval  27873  lnosub  27894  dipsubdir  27983  sspph  27990  hvadd4  28173  hvpncan  28176  his35  28225  hiassdi  28228  shscli  28456  shmodsi  28528  chj4  28674  spansnmul  28703  spansncol  28707  spanunsni  28718  hoadd4  28923  hosubadd4  28953  lnopl  29053  unopf1o  29055  counop  29060  lnfnl  29070  hmopadj2  29080  eighmre  29102  lnopmi  29139  lnophsi  29140  hmops  29159  hmopm  29160  cnlnadjlem2  29207  adjmul  29231  adjadd  29232  kbass6  29260  mdslj1i  29458  mdslj2i  29459  mdslmd1lem1  29464  mdslmd2i  29469  chirredlem3  29531  isoun  29759  xdivmul  29913  odutos  29943  isarchi2  30019  archiabllem2  30031  metider  30217  pl1cn  30281  rossros  30523  ismeas  30542  dya2iocnei  30624  inelcarsg  30653  bnj563  31091  cnpconn  31490  cvmseu  31536  elmrsubrn  31695  mrsubco  31696  subdivcomb1  31889  nosupbnd2  32139  fneint  32620  fnessref  32629  tailfb  32649  onsucuni3  33497  ptrecube  33691  poimirlem4  33695  heicant  33726  mblfinlem1  33728  mblfinlem2  33729  mblfinlem3  33730  mblfinlem4  33731  cnambfre  33740  itg2addnclem2  33744  ftc1anclem5  33771  ftc1anclem6  33772  metf1o  33833  isbnd3b  33866  equivbnd  33871  heiborlem3  33894  rrnmet  33910  rrndstprj1  33911  rrntotbnd  33917  exidcl  33957  ghomco  33972  ghomdiv  33973  grpokerinj  33974  rngoneglmul  34024  rngonegrmul  34025  rngosubdi  34026  rngosubdir  34027  isdrngo2  34039  rngohomco  34055  rngoisocnv  34062  riscer  34069  crngm4  34084  crngohomfo  34087  idlsubcl  34104  inidl  34111  keridl  34113  ispridlc  34151  pridlc3  34154  dmncan1  34157  lflvscl  34836  3dim0  35215  linepsubN  35510  cdlemg2fvlem  36353  trlcoat  36482  istendod  36521  dva1dim  36744  dvhvaddcomN  36856  dihf11  37027  dihlatat  37097  ismrc  37735  isnacs3  37744  mzpindd  37780  pellex  37870  monotoddzzfi  37978  lermxnn0  37988  rmyeq0  37991  rmyeq  37992  lermy  37993  jm2.27  38046  lsmfgcl  38115  fsumcnsrcl  38207  rngunsnply  38214  isdomn3  38253  gsumws3  38970  nzin  38988  ofdivrec  38996  ofdivcan4  38997  chordthmALT  39637  projf1o  39854  ltdiv23neg  40084  fmulcl  40285  rrxdsfi  40977  ismgmd  42255  idmgmhm  42267  resmgmhm  42277  resmgmhm2  42278  resmgmhm2b  42279  mgmhmco  42280  mgmhmima  42281  submgmacs  42283  mgmplusgiopALT  42309  c0mgm  42388  c0mhm  42389
  Copyright terms: Public domain W3C validator