MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expa Unicode version

Theorem 3expa 1196
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3expa

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3
213exp 1195 . 2
32imp31 432 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3anidm23  1287  mp3an2  1312  mpd3an3  1325  rgen3  2883  moi2  3280  sbc3ie  3405  2if2  3989  preq12bg  4209  prel12g  4210  reuhypd  4679  otsndisj  4757  fvtp1g  6121  f1imass  6172  weisoeq  6251  f1ofveu  6291  f1ocnvfv3  6292  curry1f  6894  curry2f  6896  funsssuppss  6945  tfrlem11  7076  oalimcl  7228  oeordsuc  7262  oelim2  7263  nneob  7320  mapxpen  7703  findcard  7779  wemaplem3  7994  en2eqpr  8406  infxpabs  8613  infxp  8616  cfflb  8660  cfsmolem  8671  isf32lem12  8765  fin1a2lem9  8809  fin1a2s  8815  axcc3  8839  axdc3lem4  8854  zornn0g  8906  pwfseqlem4  9061  tskwun  9183  tskint  9184  tskxp  9186  tskmap  9187  gruf  9210  gruwun  9212  grutsk1  9220  addcanpi  9298  ltapi  9302  mul4  9770  add4  9817  2addsub  9857  addsubeq4  9858  muladd  10014  ltleadd  10060  receu  10219  p1le  10410  lemul12b  10424  lbinfm  10521  zdiv  10958  fzind  10987  fnn0ind  10988  uzss  11130  zbtwnre  11209  qmulcl  11229  qreccl  11231  xrlttr  11375  xaddass  11470  xmulasslem3  11507  xmulass  11508  xadddilem  11515  xrsupsslem  11527  xrinfmsslem  11528  supxrunb1  11540  ixxin  11575  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  iooshf  11632  prunioo  11678  ioojoin  11680  elfz5  11709  elfz0fzfz0  11808  elfzonelfzo  11912  fzind2  11924  mulexpz  12206  expsub  12213  digit2  12299  digit1  12300  facndiv  12366  faclbnd4lem4  12374  faclbnd4  12375  faclbnd5  12376  bccmpl  12387  bcval5  12396  bcpasc  12399  hashunx  12454  ccatrn  12606  swrdspsleq  12673  swrdccat1  12682  swrdccat2  12683  swrdswrd  12685  cats1un  12701  crim  12948  absmax  13162  ello12r  13340  elo12r  13351  climshftlem  13397  2sumeq2dv  13527  expcnv  13675  2cprodeq2dv  13732  rpnnen2lem7  13954  dvdsval3  13990  dvdsnegb  14001  muldvds1  14008  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  dvdsmulcr  14013  dvds2ln  14014  divalgb  14062  ndvdssub  14065  gcddiv  14187  rpexp1i  14262  phiprmpw  14306  pythagtriplem1  14340  pockthg  14424  infpnlem1  14428  4sqlem3  14468  0ramcl  14541  firest  14830  imasaddfnlem  14925  imasleval  14938  xpsfrn2  14967  mrerintcl  14994  iscatd  15070  clatleglb  15756  mreclatBAD  15817  pslem  15836  mrcmndind  15997  grplmulf1o  16112  grplactcnv  16138  mulgnn0subcl  16155  mulgsubcl  16156  mulgdir  16167  issubg2  16216  issubgrpd2  16217  cycsubgcl  16227  cycsubgss  16228  nmzsubg  16242  eqgen  16254  ghmmulg  16279  conjghm  16297  symgfixfo  16464  odeq  16574  odval2  16575  odf1  16584  dfod2  16586  gexdvds  16604  gexdvds2  16605  gexcl2  16609  gexdvds3  16610  sylow2blem2  16641  efgsp1  16755  efgrelexlemb  16768  mulgmhm  16836  mulgghm  16837  iscyggen2  16884  iscyg3  16889  srglmhm  17186  srgrmhm  17187  ringlghm  17250  ringrghm  17251  gsumdixpOLD  17257  gsumdixp  17258  dvdsrcl2  17299  crngunit  17311  kerf1hrm  17392  subrgugrp  17448  cntzsubr  17461  lmodvsdir  17536  lmodvsass  17537  lmodvsghm  17571  lsssubg  17603  lss1d  17609  islbs2  17800  lidlsubg  17862  lidlsubcl  17863  quscrng  17888  lpigen  17904  xrsdsreval  18463  expghm  18529  expghmOLD  18530  mulgghm2  18531  mulgghm2OLD  18534  ip0r  18672  obs2ss  18760  islindf3  18861  scmatscm  19015  scmataddcl  19018  scmatsubcl  19019  scmatfo  19032  matunit  19180  cpmatelimp  19213  cpmatelimp2  19215  cpmatinvcl  19218  cpmatmcl  19220  mat2pmatf  19229  m2cpmf  19243  cpm2mf  19253  m2cpmfo  19257  m2cpminv  19261  decpmataa0  19269  pm2mpf  19299  pm2mpf1  19300  idpm2idmp  19302  pm2mpfo  19315  elcls2  19575  opnnei  19621  innei  19626  iscnp4  19764  cnpnei  19765  iscncl  19770  cnnei  19783  cnconst  19785  ordthauslem  19884  bwth  19910  1stccnp  19963  llyrest  19986  nllyrest  19987  kgenss  20044  xkoccn  20120  kqsat  20232  kqt0lem  20237  isr0  20238  fbssfi  20338  isfild  20359  filcon  20384  trfilss  20390  fgtr  20391  ufileu  20420  ufilen  20431  fmfnfmlem4  20458  fmfnfm  20459  hausflimi  20481  cnpflf2  20501  cnpflf  20502  cnflf  20503  cnpfcf  20542  cnfcf  20543  cnextcn  20567  tmdmulg  20591  clsnsg  20608  tsmsxplem1  20655  tsmsxp  20657  trust  20732  ustuqtop0  20743  ismeti  20828  isxmet2d  20830  elbl2ps  20892  elbl2  20893  xblpnfps  20898  xblpnf  20899  xbln0  20917  blin  20924  blssexps  20929  blssex  20930  blsscls2  21007  blcls  21009  blsscls  21010  metss  21011  metrest  21027  metcn  21046  metustblOLD  21083  metustbl  21084  metutopOLD  21085  psmetutop  21086  nmf2  21113  nmdvr  21179  nmoi  21235  nmoix  21236  nmoleub  21238  nghmcn  21252  xrsxmet  21314  iccntr  21326  metdsle  21356  icoopnst  21439  iocopnst  21440  icccvx  21450  pi1xfr  21555  lmmbr  21697  lmmbr2  21698  iscfil3  21712  iscau2  21716  cfilres  21735  bcthlem1  21763  bcthlem4  21766  bcthlem5  21767  rrxmet  21835  ioombl  21975  iccvolcl  21977  ioovolcl  21979  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  ig1pcl  22576  ig1prsp  22578  aannenlem1  22724  taylplem1  22758  dvtaylp  22765  relogeftb  22969  logdivlt  23006  cxpexp  23049  rpcxpcl  23057  isppw2  23389  vmappw  23390  lgslem4  23574  lgscllem  23578  lgsneg1  23595  lgsne0  23608  brbtwn2  24208  ax5seglem1  24231  ax5seglem2  24232  axcontlem4  24270  nbgraf1olem5  24445  constr3cycl  24661  wwlknimp  24687  usg2wlkeq  24708  wwlknred  24723  wwlknext  24724  clwwlknprop  24772  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  4cycl2vnunb  25017  frgrancvvdeqlemB  25038  usgreghash2spotv  25066  2spotmdisj  25068  grpoidinvlem3  25208  isvci  25475  nmcvcn  25605  ipval2lem2  25614  ipval2lem5  25620  sspival  25651  sspimsval  25653  isblo2  25698  nmoo0  25706  blocni  25720  isph  25737  sspph  25770  hvadd4  25953  hiassdi  26008  ocsh  26201  chj4  26453  spansncol  26486  pjjsi  26618  hoscl  26664  hodcl  26666  hoadd4  26703  homco1  26720  homulass  26721  hoadddi  26722  hoadddir  26723  unoplin  26839  adjvalval  26856  hmoplin  26861  bralnfn  26867  brafnmul  26870  lnopmi  26919  lnopcoi  26922  hmops  26939  hmopm  26940  nmophmi  26950  lnfncnbd  26976  cnlnadjlem2  26987  adjlnop  27005  adjmul  27011  adjadd  27012  branmfn  27024  kbass5  27039  kbass6  27040  leop2  27043  leopadd  27051  leopmuli  27052  pjimai  27095  atcvatlem  27304  chirredlem2  27310  mdsymlem3  27324  mdsymlem5  27326  sumdmdii  27334  sumdmdlem  27337  cdj3lem2a  27355  cdj3lem2b  27356  cdj3lem3a  27358  cdj3i  27360  xreceu  27618  toslublem  27655  tosglblem  27657  ogrpaddltbi  27709  archiabllem1b  27736  archiabllem2c  27739  archiabl  27742  slmdvsdir  27759  slmdvsass  27760  pstmxmet  27876  ordtconlem1  27906  hasheuni  28091  ballotlemirc  28470  signswmnd  28514  txpcon  28677  cvmscld  28718  elmpps  28933  dfrdg2  29228  wsuclem  29381  nobndlem8  29459  segconeu  29661  linecom  29800  linethru  29803  lineintmo  29807  heicant  30049  mblfinlem1  30051  mblfinlem3  30053  ismblfin  30055  cnambfre  30063  itg2addnclem2  30067  ftc1anclem1  30090  ftc1anclem5  30094  ftc1anclem6  30095  ftc2nc  30099  areacirclem2  30108  areacirclem4  30110  areacirclem5  30111  areacirc  30112  fnemeet2  30185  fnejoin2  30187  fzmul  30233  subspopn  30245  isbndx  30278  isbnd2  30279  isbnd3  30280  ssbnd  30284  prdstotbnd  30290  heibor1  30306  rrnmet  30325  rngonegmn1l  30352  rngohomco  30377  rngoisocnv  30384  rngoisoco  30385  crngohomfo  30403  isidlc  30412  rngoidl  30421  prnc  30464  ispridlc  30467  oddcomabszz  30880  acongtr  30916  rpnnen3lem  30973  islssfg  31016  lmhmfgsplit  31032  unxpwdom3  31041  hbtlem7  31074  sdrgacs  31150  hashgcdeq  31158  iocmbl  31180  nzss  31222  dvconstbi  31239  bccbc  31250  uzmptshftfval  31251  iccdifprioo  31556  dvnmul  31740  fourierdlem74  31963  fourierdlem75  31964  ralxfrd2  32303  el2fzo  32339  usgra2pthlem1  32353  fullestrcsetc  32657  fullsetcestrc  32672  rnghmsubcsetclem2  32784  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  lcoss  33037  snlindsntorlem  33071  aacllem  33216  bnj1204  34068  cvrval2  34999  glbconxN  35102  hlrelat5N  35125  cvratlem  35145  cvrat2  35153  athgt  35180  3dim2  35192  llnn0  35240  lplnn0N  35271  lvoln0N  35315  snatpsubN  35474  paddasslem18  35561  pmod1i  35572  lhpexle2  35734  lhpexle3lem  35735  lhpexle3  35736  ldilcnv  35839  trlcnv  35890  trlnidatb  35902  cdleme32snaw  36161  cdleme32fvaw  36165  cdleme42ke  36211  cdlemeg46gf  36259  cdleme50trn12  36278  cdlemg1cex  36314  cdlemb3  36332  tgrpgrplem  36475  tgrpabl  36477  tendoplcl2  36504  tendo0pl  36517  tendoicl  36522  tendoipl  36523  cdlemkid3N  36659  tendoex  36701  erngdvlem4  36717  erngdvlem4-rN  36725  dib1dim  36892  dib1dim2  36895  dihglbcpreN  37027  dihmeetALTN  37054  dih1dimatlem  37056  dihatlat  37061
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator