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

Theorem 3expb 1285
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 1283 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 448 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  3adant3r1  1295  3adant3r2  1296  3adant3r3  1297  3adant1l  1358  3adant1r  1359  mp3an1  1451  sotri  5558  fnfco  6107  mpt2eq3dva  6761  oprres  6844  fovrnda  6847  grprinvd  6915  fnmpt2ovd  7297  offval22  7298  bropfvvvvlem  7301  fnsuppres  7367  suppsssn  7375  sprmpt2d  7395  oaass  7686  omlimcl  7703  odi  7704  nnmsucr  7750  cflim2  9123  mulcanenq  9820  mul4  10243  add4  10294  2addsub  10333  addsubeq4  10334  subadd4  10363  muladd  10500  ltleadd  10549  divmul  10726  divne0  10735  div23  10742  div12  10745  divsubdir  10759  divcan5  10765  divmuleq  10768  divcan6  10770  divdiv32  10771  div2sub  10888  letrp1  10903  lemul12b  10918  lediv1  10926  lt2mul2div  10939  lemuldiv  10941  ltdiv2  10947  ledivdiv  10950  lediv2  10951  ltdiv23  10952  lediv23  10953  sup2  11017  cju  11054  nndivre  11094  nndivtr  11100  nn0addge1  11377  nn0addge2  11378  peano2uz2  11503  uzind  11507  uzind3  11509  fzind  11513  fnn0ind  11514  uzind4  11784  qre  11831  irrmul  11851  rpdivcl  11894  rerpdivcl  11899  xrinfmsslem  12176  ixxin  12230  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  fzaddel  12413  fzadd2  12414  fzrev  12441  modlt  12719  modcyc  12745  axdc4uzlem  12822  expdiv  12951  fundmge2nop0  13312  swrd00  13463  swrdcl  13464  swrd0  13480  swrdccat  13539  swrdco  13629  2shfti  13864  isermulc2  14432  fsummulc2  14560  dvdscmulr  15057  dvdsmulcr  15058  dvds2add  15062  dvds2sub  15063  dvdstr  15065  alzdvds  15089  divalg2  15175  dvdslegcd  15273  lcmgcdlem  15366  lcmgcdeq  15372  isprm6  15473  pcqcl  15608  vdwmc2  15730  ressinbas  15983  cicer  16513  isposd  17002  pleval2i  17011  tosso  17083  poslubmo  17193  posglbmo  17194  mgmplusf  17298  ismndd  17360  imasmnd2  17374  idmhm  17391  issubm2  17395  0mhm  17405  resmhm  17406  resmhm2  17407  resmhm2b  17408  mhmco  17409  mhmima  17410  submacs  17412  prdspjmhm  17414  pwsdiagmhm  17416  pwsco1mhm  17417  pwsco2mhm  17418  gsumwsubmcl  17422  gsumccat  17425  gsumwmhm  17429  grpinvcnv  17530  grpinvnzcl  17534  grpsubf  17541  imasgrp2  17577  qusgrp2  17580  mhmfmhm  17585  mulgnnsubcl  17600  mulgnndir  17616  mulgnndirOLD  17617  issubg4  17660  isnsg3  17675  nsgacs  17677  nsgid  17687  qusadd  17698  ghmmhm  17717  ghmmhmb  17718  idghm  17722  resghm  17723  ghmf1  17736  qusghm  17744  gaid  17778  subgga  17779  gasubg  17781  invoppggim  17836  gsmsymgrfix  17894  lsmidm  18123  pj1ghm  18162  mulgnn0di  18277  mulgmhm  18279  mulgghm  18280  ghmfghm  18282  invghm  18285  ghmplusg  18295  ablnsg  18296  qusabl  18314  gsumval3eu  18351  gsumval3  18354  gsumzcl2  18357  gsumzaddlem  18367  gsumzadd  18368  gsumzmhm  18383  gsumzoppg  18390  srgfcl  18561  srgmulgass  18577  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  issubrg2  18848  issrngd  18909  islmodd  18917  lmodscaf  18933  lcomf  18950  lmodvsghm  18972  rmodislmodlem  18978  lssacs  19015  idlmhm  19089  invlmhm  19090  lmhmvsca  19093  reslmhm2  19101  reslmhm2b  19102  pwsdiaglmhm  19105  pwssplit2  19108  pwssplit3  19109  issubrngd2  19237  qusrhm  19285  crngridl  19286  quscrng  19288  isnzr2  19311  domnmuln0  19346  opprdomn  19349  asclghm  19386  asclrhm  19390  psraddcl  19431  psrvscacl  19441  psrass23  19458  psrbagev1  19558  coe1sclmulfv  19701  cply1mul  19712  expmhm  19863  zntoslem  19953  znfld  19957  psgnghm  19974  phlipf  20045  frlmup1  20185  mndvcl  20245  matbas2d  20277  submaeval  20436  minmar1eval  20503  cpmatacl  20569  pmatcollpw1  20629  pmatcollpw  20634  tgclb  20822  topbas  20824  ntrss  20907  mretopd  20944  neissex  20979  cnpnei  21116  lmcnp  21156  ordthaus  21236  llynlly  21328  restnlly  21333  llyidm  21339  nllyidm  21340  ptbasin  21428  txcnp  21471  ist0-4  21580  kqt0lem  21587  isr0  21588  regr1lem2  21591  cmphmph  21639  connhmph  21640  fbun  21691  trfbas2  21694  isfil2  21707  isfild  21709  infil  21714  fbasfip  21719  fbasrn  21735  trfil2  21738  rnelfmlem  21803  fmfnfmlem3  21807  flimopn  21826  txflf  21857  fclsnei  21870  fclsfnflim  21878  fcfnei  21886  clssubg  21959  tgphaus  21967  qustgplem  21971  tsmsadd  21997  psmetxrge0  22165  psmetlecl  22167  xmetlecl  22198  xmettpos  22201  imasdsf1olem  22225  imasf1oxmet  22227  imasf1omet  22228  elbl3ps  22243  elbl3  22244  metss  22360  comet  22365  stdbdxmet  22367  stdbdmet  22368  methaus  22372  nrmmetd  22426  abvmet  22427  isngp4  22463  subgngp  22486  nmoi2  22581  nmoleub  22582  nmoid  22593  bl2ioo  22642  zcld  22663  divcn  22718  divccn  22723  cncffvrn  22748  divccncf  22756  icoopnst  22785  clmzlmvsca  22959  cph2ass  23059  tchcph  23082  cfilfcls  23118  bcthlem2  23168  rrxmet  23237  rrxdstprj1  23238  cldcss  23258  dvrec  23763  dvmptfsum  23783  aalioulem3  24134  taylply2  24167  efsubm  24342  dchrelbasd  25009  dchrmulcl  25019  pntrmax  25298  padicabv  25364  axtgcont  25413  xmstrkgc  25811  axsegconlem1  25842  axlowdimlem15  25881  usgredg2vlem1  26162  usgredg2vlem2  26163  iswlkon  26609  wlknwwlksninj  26843  wwlksnextsur  26863  elwwlks2  26933  elwspths2spth  26934  frrusgrord  27321  numclwlk1lem2foalem  27341  grpoidinvlem2  27487  grpoidinvlem3  27488  ablo4  27532  ablomuldiv  27534  nvaddsub4  27640  nvmeq0  27641  sspmval  27716  sspimsval  27721  lnosub  27742  dipsubdir  27831  sspph  27838  hvadd4  28021  hvpncan  28024  his35  28073  hiassdi  28076  shscli  28304  shmodsi  28376  chj4  28522  spansnmul  28551  spansncol  28555  spanunsni  28566  hoadd4  28771  hosubadd4  28801  lnopl  28901  unopf1o  28903  counop  28908  lnfnl  28918  hmopadj2  28928  eighmre  28950  lnopmi  28987  lnophsi  28988  hmops  29007  hmopm  29008  cnlnadjlem2  29055  adjmul  29079  adjadd  29080  kbass6  29108  mdslj1i  29306  mdslj2i  29307  mdslmd1lem1  29312  mdslmd2i  29317  chirredlem3  29379  isoun  29607  xdivmul  29761  odutos  29791  isarchi2  29867  archiabllem2  29879  metider  30065  pl1cn  30129  rossros  30371  ismeas  30390  dya2iocnei  30472  inelcarsg  30501  bnj563  30939  cnpconn  31338  cvmseu  31384  elmrsubrn  31543  mrsubco  31544  subdivcomb1  31737  nosupbnd2  31987  fneint  32468  fnessref  32477  tailfb  32497  onsucuni3  33345  ptrecube  33539  poimirlem4  33543  heicant  33574  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  cnambfre  33588  itg2addnclem2  33592  ftc1anclem5  33619  ftc1anclem6  33620  metf1o  33681  isbnd3b  33714  equivbnd  33719  heiborlem3  33742  rrnmet  33758  rrndstprj1  33759  rrntotbnd  33765  exidcl  33805  ghomco  33820  ghomdiv  33821  grpokerinj  33822  rngoneglmul  33872  rngonegrmul  33873  rngosubdi  33874  rngosubdir  33875  isdrngo2  33887  rngohomco  33903  rngoisocnv  33910  riscer  33917  crngm4  33932  crngohomfo  33935  idlsubcl  33952  inidl  33959  keridl  33961  ispridlc  33999  pridlc3  34002  dmncan1  34005  lflvscl  34682  3dim0  35061  linepsubN  35356  cdlemg2fvlem  36199  trlcoat  36328  istendod  36367  dva1dim  36590  dvhvaddcomN  36702  dihf11  36873  dihlatat  36943  ismrc  37581  isnacs3  37590  mzpindd  37626  pellex  37716  monotoddzzfi  37824  lermxnn0  37834  rmyeq0  37837  rmyeq  37838  lermy  37839  jm2.27  37892  lsmfgcl  37961  fsumcnsrcl  38053  rngunsnply  38060  isdomn3  38099  gsumws3  38816  nzin  38834  ofdivrec  38842  ofdivcan4  38843  chordthmALT  39483  projf1o  39700  ltdiv23neg  39930  fmulcl  40131  rrxdsfi  40823  ismgmd  42101  idmgmhm  42113  resmgmhm  42123  resmgmhm2  42124  resmgmhm2b  42125  mgmhmco  42126  mgmhmima  42127  submgmacs  42129  mgmplusgiopALT  42155  c0mgm  42234  c0mhm  42235
  Copyright terms: Public domain W3C validator