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

Theorem 3expb 1142
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 1141 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 407 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3expia  1143  3adant1lOLD  1215  3adant1rOLD  1217  3adant3r1  1226  3adant3r2  1227  3adant3r3  1228  mp3an1  1565  sotri  5748  fnfco  6294  mpt2eq3dva  6959  oprres  7042  fovrnda  7045  grprinvd  7113  fnmpt2ovd  7495  fnmpt2ovdOLD  7496  offval22  7497  bropfvvvvlem  7500  fnsuppres  7567  suppsssn  7575  sprmpt2d  7595  oaass  7888  omlimcl  7905  odi  7906  nnmsucr  7952  cflim2  9380  mulcanenq  10077  mul4  10500  add4  10551  2addsub  10590  addsubeq4  10591  subadd4  10620  muladd  10757  ltleadd  10806  divmul  10983  divne0  10992  div23  10999  div12  11002  divsubdir  11016  divcan5  11022  divmuleq  11025  divcan6  11027  divdiv32  11028  div2sub  11145  letrp1  11160  lemul12b  11175  lediv1  11183  lt2mul2div  11196  lemuldiv  11198  ltdiv2  11204  ledivdiv  11207  lediv2  11208  ltdiv23  11209  lediv23  11210  sup2  11274  cju  11311  nndivre  11354  nndivtr  11360  nn0addge1  11625  nn0addge2  11626  peano2uz2  11751  uzind  11755  uzind3  11757  fzind  11761  fnn0ind  11762  uzind4  11984  qre  12032  irrmul  12052  rpdivcl  12090  rerpdivcl  12095  xrinfmsslem  12376  ixxin  12430  iccshftr  12549  iccshftl  12551  iccdil  12553  icccntr  12555  fzaddel  12618  fzadd2  12619  fzrev  12646  modlt  12923  modcyc  12949  axdc4uzlem  13026  expdiv  13154  fundmge2nop0  13511  swrd00  13661  swrdcl  13662  swrd0  13678  swrdccat  13737  swrdco  13827  2shfti  14063  isermulc2  14631  fsummulc2  14758  dvdscmulr  15253  dvdsmulcr  15254  dvds2add  15258  dvds2sub  15259  dvdstr  15261  alzdvds  15285  divalg2  15368  dvdslegcd  15465  lcmgcdlem  15558  lcmgcdeq  15564  isprm6  15663  pcqcl  15798  vdwmc2  15920  ressinbas  16167  cicer  16690  isposd  17180  pleval2i  17189  tosso  17261  poslubmo  17371  posglbmo  17372  mgmplusf  17476  ismndd  17538  imasmnd2  17552  idmhm  17569  issubm2  17573  0mhm  17583  resmhm  17584  resmhm2  17585  resmhm2b  17586  mhmco  17587  mhmima  17588  submacs  17590  prdspjmhm  17592  pwsdiagmhm  17594  pwsco1mhm  17595  pwsco2mhm  17596  gsumwsubmcl  17600  gsumccat  17603  gsumwmhm  17607  grpinvcnv  17708  grpinvnzcl  17712  grpsubf  17719  imasgrp2  17755  qusgrp2  17758  mhmfmhm  17763  mulgnnsubcl  17778  mulgnndir  17793  issubg4  17835  isnsg3  17850  nsgacs  17852  nsgid  17862  qusadd  17873  ghmmhm  17892  ghmmhmb  17893  idghm  17897  resghm  17898  ghmf1  17911  qusghm  17919  gaid  17953  subgga  17954  gasubg  17956  invoppggim  18011  gsmsymgrfix  18069  lsmidm  18298  pj1ghm  18337  mulgnn0di  18452  mulgmhm  18454  mulgghm  18455  ghmfghm  18457  invghm  18460  ghmplusg  18470  ablnsg  18471  qusabl  18489  gsumval3eu  18526  gsumval3  18529  gsumzcl2  18532  gsumzaddlem  18542  gsumzadd  18543  gsumzmhm  18558  gsumzoppg  18565  srgfcl  18737  srgmulgass  18753  srglmhm  18757  srgrmhm  18758  ringlghm  18826  ringrghm  18827  issubrg2  19024  issrngd  19085  islmodd  19093  lmodscaf  19109  lcomf  19126  lmodvsghm  19148  rmodislmodlem  19154  lssacs  19194  idlmhm  19268  invlmhm  19269  lmhmvsca  19272  reslmhm2  19280  reslmhm2b  19281  pwsdiaglmhm  19284  pwssplit2  19287  pwssplit3  19288  issubrngd2  19418  qusrhm  19466  crngridl  19467  quscrng  19469  isnzr2  19492  domnmuln0  19527  opprdomn  19530  asclghm  19567  asclrhm  19571  psraddcl  19612  psrvscacl  19622  psrass23  19639  psrbagev1  19738  coe1sclmulfv  19881  cply1mul  19892  expmhm  20043  zntoslem  20132  znfld  20136  psgnghm  20153  phlipf  20227  frlmup1  20368  mndvcl  20428  matbas2d  20460  submaeval  20620  minmar1eval  20687  cpmatacl  20755  pmatcollpw1  20815  pmatcollpw  20820  tgclb  21009  topbas  21011  ntrss  21094  mretopd  21131  neissex  21166  cnpnei  21303  lmcnp  21343  ordthaus  21423  llynlly  21515  restnlly  21520  llyidm  21526  nllyidm  21527  ptbasin  21615  txcnp  21658  ist0-4  21767  kqt0lem  21774  isr0  21775  regr1lem2  21778  cmphmph  21826  connhmph  21827  fbun  21878  trfbas2  21881  isfil2  21894  isfild  21896  infil  21901  fbasfip  21906  fbasrn  21922  trfil2  21925  rnelfmlem  21990  fmfnfmlem3  21994  flimopn  22013  txflf  22044  fclsnei  22057  fclsfnflim  22065  fcfnei  22073  clssubg  22146  tgphaus  22154  qustgplem  22158  tsmsadd  22184  psmetxrge0  22352  psmetlecl  22354  xmetlecl  22385  xmettpos  22388  imasdsf1olem  22412  imasf1oxmet  22414  imasf1omet  22415  elbl3ps  22430  elbl3  22431  metss  22547  comet  22552  stdbdxmet  22554  stdbdmet  22555  methaus  22559  nrmmetd  22613  abvmet  22614  isngp4  22650  subgngp  22673  nmoi2  22768  nmoleub  22769  nmoid  22780  bl2ioo  22829  zcld  22850  divcn  22905  divccn  22910  cncffvrn  22935  divccncf  22943  icoopnst  22972  clmzlmvsca  23146  cph2ass  23246  tchcph  23269  cfilfcls  23306  bcthlem2  23356  rrxmet  23426  rrxdstprj1  23427  cldcss  23447  dvrec  23955  dvmptfsum  23975  aalioulem3  24326  taylply2  24359  efsubm  24535  dchrelbasd  25201  dchrmulcl  25211  pntrmax  25490  padicabv  25556  axtgcont  25605  xmstrkgc  26003  axsegconlem1  26034  axlowdimlem15  26073  usgredg2vlem1  26355  usgredg2vlem2  26356  iswlkon  26804  wlknwwlksninjOLD  27039  wwlksnextsur  27060  elwwlks2  27131  elwspths2spth  27132  frrusgrord  27539  numclwwlk1lem2foalem  27553  grpoidinvlem2  27711  grpoidinvlem3  27712  ablo4  27756  ablomuldiv  27758  nvaddsub4  27863  nvmeq0  27864  sspmval  27939  sspimsval  27944  lnosub  27965  dipsubdir  28054  sspphOLD  28061  hvadd4  28244  hvpncan  28247  his35  28296  hiassdi  28299  shscli  28527  shmodsi  28599  chj4  28745  spansnmul  28774  spansncol  28778  spanunsni  28789  hoadd4  28994  hosubadd4  29024  lnopl  29124  unopf1o  29126  counop  29131  lnfnl  29141  hmopadj2  29151  eighmre  29173  lnopmi  29210  lnophsi  29211  hmops  29230  hmopm  29231  cnlnadjlem2  29278  adjmul  29302  adjadd  29303  kbass6  29331  mdslj1i  29529  mdslj2i  29530  mdslmd1lem1  29535  mdslmd2i  29540  chirredlem3  29602  isoun  29829  xdivmul  29981  odutos  30011  isarchi2  30087  archiabllem2  30099  metider  30285  pl1cn  30349  rossros  30591  ismeas  30610  dya2iocnei  30692  inelcarsg  30721  bnj563  31158  cnpconn  31557  cvmseu  31603  elmrsubrn  31762  mrsubco  31763  subdivcomb1  31955  nosupbnd2  32205  fneint  32686  fnessref  32695  tailfb  32715  onsucuni3  33550  ptrecube  33741  poimirlem4  33745  heicant  33776  mblfinlem1  33778  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  cnambfre  33789  itg2addnclem2  33793  ftc1anclem5  33820  ftc1anclem6  33821  metf1o  33881  isbnd3b  33914  equivbnd  33919  heiborlem3  33942  rrnmet  33958  rrndstprj1  33959  rrntotbnd  33965  exidcl  34005  ghomco  34020  ghomdiv  34021  grpokerinj  34022  rngoneglmul  34072  rngonegrmul  34073  rngosubdi  34074  rngosubdir  34075  isdrngo2  34087  rngohomco  34103  rngoisocnv  34110  riscer  34117  crngm4  34132  crngohomfo  34135  idlsubcl  34152  inidl  34159  keridl  34161  ispridlc  34199  pridlc3  34202  dmncan1  34205  lflvscl  34876  3dim0  35256  linepsubN  35551  cdlemg2fvlem  36393  trlcoat  36522  istendod  36561  dva1dim  36784  dvhvaddcomN  36895  dihf11  37066  dihlatat  37136  ismrc  37784  isnacs3  37793  mzpindd  37829  pellex  37919  monotoddzzfi  38026  lermxnn0  38036  rmyeq0  38039  rmyeq  38040  lermy  38041  jm2.27  38094  lsmfgcl  38163  fsumcnsrcl  38255  rngunsnply  38262  isdomn3  38301  gsumws3  39017  nzin  39035  ofdivrec  39043  ofdivcan4  39044  chordthmALT  39681  projf1o  39893  ltdiv23neg  40114  fmulcl  40311  rrxdsfi  41002  ismgmd  42362  idmgmhm  42374  resmgmhm  42384  resmgmhm2  42385  resmgmhm2b  42386  mgmhmco  42387  mgmhmima  42388  submgmacs  42390  mgmplusgiopALT  42416  c0mgm  42495  c0mhm  42496
  Copyright terms: Public domain W3C validator