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

Theorem 3expb 1257
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 1255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 447 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3adant3r1  1265  3adant3r2  1266  3adant3r3  1267  3adant1l  1309  3adant1r  1310  mp3an1  1402  sotri  5429  fnfco  5967  mpt2eq3dva  6595  oprres  6678  fovrnda  6681  grprinvd  6749  fnmpt2ovd  7117  offval22  7118  bropfvvvvlem  7121  fnsuppres  7187  suppsssn  7195  sprmpt2d  7215  oaass  7506  omlimcl  7523  odi  7524  nnmsucr  7570  cflim2  8946  mulcanenq  9639  mul4  10057  add4  10108  2addsub  10147  addsubeq4  10148  subadd4  10177  muladd  10314  ltleadd  10363  divmul  10540  divne0  10549  div23  10556  div12  10559  divsubdir  10573  divcan5  10579  divmuleq  10582  divcan6  10584  divdiv32  10585  div2sub  10702  letrp1  10717  lemul12b  10732  lediv1  10740  lt2mul2div  10753  lemuldiv  10755  ltdiv2  10761  ledivdiv  10764  lediv2  10765  ltdiv23  10766  lediv23  10767  sup2  10831  cju  10866  nndivre  10906  nndivtr  10912  nn0addge1  11189  nn0addge2  11190  peano2uz2  11300  uzind  11304  uzind3  11306  fzind  11310  fnn0ind  11311  uzind4  11581  qre  11628  irrmul  11648  rpdivcl  11691  rerpdivcl  11696  xrinfmsslem  11969  ixxin  12022  iccshftr  12136  iccshftl  12138  iccdil  12140  icccntr  12142  fzaddel  12204  fzadd2  12205  fzrev  12231  modlt  12499  modcyc  12525  axdc4uzlem  12602  expdiv  12731  swrd00  13219  swrdcl  13220  swrd0  13235  swrdccat  13293  swrdco  13383  2shfti  13617  isermulc2  14185  fsummulc2  14307  dvdscmulr  14797  dvdsmulcr  14798  dvds2add  14802  dvds2sub  14803  dvdstr  14805  alzdvds  14829  divalg2  14915  dvdslegcd  15013  lcmgcdlem  15106  lcmgcdeq  15112  isprm6  15213  pcqcl  15348  vdwmc2  15470  ressinbas  15712  cicer  16238  isposd  16727  pleval2i  16736  tosso  16808  poslubmo  16918  posglbmo  16919  mgmplusf  17023  ismndd  17085  imasmnd2  17099  idmhm  17116  issubm2  17120  0mhm  17130  resmhm  17131  resmhm2  17132  resmhm2b  17133  mhmco  17134  mhmima  17135  submacs  17137  prdspjmhm  17139  pwsdiagmhm  17141  pwsco1mhm  17142  pwsco2mhm  17143  gsumwsubmcl  17147  gsumccat  17150  gsumwmhm  17154  grpinvcnv  17255  grpinvnzcl  17259  grpsubf  17266  imasgrp2  17302  qusgrp2  17305  mhmfmhm  17310  mulgnnsubcl  17325  mulgnndir  17341  mulgnndirOLD  17342  issubg4  17385  isnsg3  17400  nsgacs  17402  nsgid  17412  qusadd  17423  ghmmhm  17442  ghmmhmb  17443  idghm  17447  resghm  17448  ghmf1  17461  qusghm  17469  gaid  17504  subgga  17505  gasubg  17507  invoppggim  17562  gsmsymgrfix  17620  lsmidm  17849  pj1ghm  17888  mulgnn0di  18003  mulgmhm  18005  mulgghm  18006  ghmfghm  18008  invghm  18011  ghmplusg  18021  ablnsg  18022  qusabl  18040  gsumval3eu  18077  gsumval3  18080  gsumzcl2  18083  gsumzaddlem  18093  gsumzadd  18094  gsumzmhm  18109  gsumzoppg  18116  srgfcl  18287  srgmulgass  18303  srglmhm  18307  srgrmhm  18308  ringlghm  18376  ringrghm  18377  issubrg2  18572  issrngd  18633  islmodd  18641  lmodscaf  18657  lcomf  18674  lmodvsghm  18696  lssacs  18737  idlmhm  18811  invlmhm  18812  lmhmvsca  18815  reslmhm2  18823  reslmhm2b  18824  pwsdiaglmhm  18827  pwssplit2  18830  pwssplit3  18831  issubrngd2  18959  qusrhm  19007  crngridl  19008  quscrng  19010  isnzr2  19033  domnmuln0  19068  opprdomn  19071  asclghm  19108  asclrhm  19112  psraddcl  19153  psrvscacl  19163  psrass23  19180  psrbagev1  19280  coe1sclmulfv  19423  cply1mul  19434  expmhm  19583  zntoslem  19672  znfld  19676  psgnghm  19693  phlipf  19764  frlmup1  19904  mndvcl  19964  matbas2d  19996  submaeval  20155  minmar1eval  20222  cpmatacl  20288  pmatcollpw1  20348  pmatcollpw  20353  tgclb  20533  topbas  20535  ntrss  20617  mretopd  20654  neissex  20689  cnpnei  20826  lmcnp  20866  ordthaus  20946  llynlly  21038  restnlly  21043  llyidm  21049  nllyidm  21050  ptbasin  21138  txcnp  21181  ist0-4  21290  kqt0lem  21297  isr0  21298  regr1lem2  21301  cmphmph  21349  conhmph  21350  fbun  21402  trfbas2  21405  isfil2  21418  isfild  21420  infil  21425  fbasfip  21430  fbasrn  21446  trfil2  21449  rnelfmlem  21514  fmfnfmlem3  21518  flimopn  21537  txflf  21568  fclsnei  21581  fclsfnflim  21589  fcfnei  21597  clssubg  21670  tgphaus  21678  qustgplem  21682  tsmsadd  21708  psmetxrge0  21876  psmetlecl  21878  xmetlecl  21909  xmettpos  21912  imasdsf1olem  21936  imasf1oxmet  21938  imasf1omet  21939  elbl3ps  21954  elbl3  21955  metss  22071  comet  22076  stdbdxmet  22078  stdbdmet  22079  methaus  22083  nrmmetd  22137  abvmet  22138  isngp4  22174  subgngp  22197  nmoi2  22292  nmoleub  22293  nmoid  22304  bl2ioo  22351  zcld  22372  divcn  22427  divccn  22432  cncffvrn  22457  divccncf  22465  icoopnst  22494  clmzlmvsca  22669  cph2ass  22766  tchcph  22789  cfilfcls  22825  bcthlem2  22875  rrxmet  22944  rrxdstprj1  22945  cldcss  22965  dvrec  23469  dvmptfsum  23487  aalioulem3  23838  taylply2  23871  efsubm  24046  dchrelbasd  24709  dchrmulcl  24719  pntrmax  24998  padicabv  25064  axtgcont  25113  xmstrkgc  25512  axsegconlem1  25543  axlowdimlem15  25582  usgraidx2vlem1  25714  usgraidx2vlem2  25715  wlknwwlkninj  26033  wwlkextsur  26053  3cyclfrgrarn  26334  frgrawopreg  26370  grpoidinvlem2  26537  grpoidinvlem3  26538  grponpncan  26578  ablo4  26585  ablomuldiv  26587  nvaddsub4  26714  nvmeq0  26717  nvelbl  26757  nvelbl2  26758  sspmval  26804  sspival  26809  sspimsval  26811  lnosub  26832  dipsubdir  26921  sspph  26928  hvadd4  27111  hvpncan  27114  his35  27163  hiassdi  27166  shscli  27394  shmodsi  27466  chj4  27612  spansnmul  27641  spansncol  27645  spanunsni  27656  hoadd4  27861  hosubadd4  27891  lnopl  27991  unopf1o  27993  counop  27998  lnfnl  28008  hmopadj2  28018  eighmre  28040  lnopmi  28077  lnophsi  28078  hmops  28097  hmopm  28098  cnlnadjlem2  28145  adjmul  28169  adjadd  28170  kbass6  28198  mdslj1i  28396  mdslj2i  28397  mdslmd1lem1  28402  mdslmd2i  28407  chirredlem3  28469  isoun  28696  xdivmul  28798  odutos  28828  isarchi2  28904  archiabllem2  28916  metider  29099  pl1cn  29163  rossros  29404  ismeas  29423  dya2iocnei  29505  inelcarsg  29534  bnj563  29901  cnpcon  30300  cvmseu  30346  elmrsubrn  30505  mrsubco  30506  subdivcomb1  30698  fneint  31347  fnessref  31356  tailfb  31376  onsucuni3  32215  ptrecube  32403  poimirlem4  32407  heicant  32438  mblfinlem1  32440  mblfinlem2  32441  mblfinlem3  32442  mblfinlem4  32443  cnambfre  32452  itg2addnclem2  32456  ftc1anclem5  32483  ftc1anclem6  32484  metf1o  32545  isbnd3b  32578  equivbnd  32583  heiborlem3  32606  rrnmet  32622  rrndstprj1  32623  rrntotbnd  32629  exidcl  32669  ghomco  32684  ghomdiv  32685  grpokerinj  32686  rngoneglmul  32736  rngonegrmul  32737  rngosubdi  32738  rngosubdir  32739  isdrngo2  32751  rngohomco  32767  rngoisocnv  32774  riscer  32781  crngm4  32796  crngohomfo  32799  idlsubcl  32816  inidl  32823  keridl  32825  ispridlc  32863  pridlc3  32866  dmncan1  32869  lflvscl  33206  3dim0  33585  linepsubN  33880  cdlemg2fvlem  34724  trlcoat  34853  istendod  34892  dva1dim  35115  dvhvaddcomN  35227  dihf11  35398  dihlatat  35468  ismrc  36106  isnacs3  36115  mzpindd  36151  pellex  36241  monotoddzzfi  36349  lermxnn0  36359  rmyeq0  36362  rmyeq  36363  lermy  36364  jm2.27  36417  lsmfgcl  36486  fsumcnsrcl  36579  rngunsnply  36586  isdomn3  36625  gsumws3  37345  nzin  37363  ofdivrec  37371  ofdivcan4  37372  chordthmALT  38015  projf1o  38205  ltdiv23neg  38382  fmulcl  38472  rrxdsfi  39005  usgredg2vlem1  40474  usgredg2vlem2  40475  upgrwlkedg  40872  iswlkOn  40887  upgr2wlk  40898  wlknwwlksninj  41108  wwlksnextsur  41128  elwwlks2  41192  elwspths2spth  41193  upgreupthi  41398  frgrwopreg  41508  frgr2wwlk1  41516  ismgmd  41588  idmgmhm  41600  resmgmhm  41610  resmgmhm2  41611  resmgmhm2b  41612  mgmhmco  41613  mgmhmima  41614  submgmacs  41616  mgmplusgiopALT  41642  c0mgm  41721  c0mhm  41722
  Copyright terms: Public domain W3C validator