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

Theorem 3expa 1215
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expa  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1214 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 438 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  3anidm23  1335  mp3an2  1361  mpd3an3  1374  rgen3  2826  moi2  3231  sbc3ie  3349  2if2  3941  preq12bg  4168  prel12g  4169  reuhypd  4641  otsndisj  4720  fvtp1g  6138  fntpb  6148  f1imass  6190  weisoeq  6271  f1ofveu  6310  f1ocnvfv3  6311  curry1f  6917  curry2f  6919  funsssuppss  6968  tfrlem11  7132  oalimcl  7287  oeordsuc  7321  oelim2  7322  nneob  7379  mapxpen  7764  findcard  7836  wemaplem3  8089  en2eqpr  8464  infxpabs  8668  infxp  8671  cfflb  8715  cfsmolem  8726  isf32lem12  8820  fin1a2lem9  8864  fin1a2s  8870  axcc3  8894  axdc3lem4  8909  zornn0g  8961  pwfseqlem4  9113  tskwun  9235  tskint  9236  tskxp  9238  tskmap  9239  gruf  9262  gruwun  9264  grutsk1  9272  addcanpi  9350  ltapi  9354  mul4  9828  add4  9875  2addsub  9915  addsubeq4  9916  muladd  10079  ltleadd  10125  receu  10285  p1le  10476  lemul12b  10490  lbinf  10587  lbinfmOLD  10588  zdiv  11035  fzind  11062  fnn0ind  11063  uzss  11208  zbtwnre  11291  qmulcl  11311  qreccl  11313  xrlttr  11468  xaddass  11564  xmulasslem3  11601  xmulass  11602  xadddilem  11609  xrsupsslem  11621  xrinfmsslem  11622  supxrunb1  11634  ixxin  11681  ioo0  11690  ico0  11711  ioc0  11712  icc0  11713  iooshf  11742  prunioo  11790  ioojoin  11792  elfz5  11821  elfz0fzfz0  11925  elfzonelfzo  12042  fzind2  12054  mulexpz  12344  expsub  12352  digit2  12437  digit1  12438  facndiv  12505  faclbnd4lem4  12513  faclbnd4  12514  faclbnd5  12515  bccmpl  12526  bcval5  12535  bcpasc  12538  hashunx  12597  ccatrn  12769  swrdccat1  12850  swrdccat2  12851  swrdswrd  12853  cats1un  12869  crim  13227  absmax  13441  ello12r  13630  elo12r  13641  climshftlem  13687  2sumeq2dv  13820  expcnv  13971  2cprodeq2dv  14028  rpnnen2lem7  14322  dvdsval3  14358  dvdsnegb  14369  muldvds1  14376  muldvds2  14377  dvdscmul  14378  dvdsmulc  14379  dvdsmulcr  14381  dvds2ln  14382  divalgb  14434  ndvdssub  14437  gcddiv  14566  lcmfval  14640  lcmfvalOLD  14644  lcmfcl  14650  dvdslcmf  14653  rpexp1i  14722  phiprmpw  14773  pythagtriplem1  14815  pockthg  14899  infpnlem1  14903  4sqlem3  14943  0ramcl  15030  firest  15380  imasaddfnlem  15483  imasleval  15496  xpsfrn2  15525  mrerintcl  15552  iscatd  15628  fullestrcsetc  16085  fullsetcestrc  16100  clatleglb  16421  mreclatBAD  16482  pslem  16501  mrcmndind  16662  grplmulf1o  16777  grplactcnv  16803  mulgnn0subcl  16820  mulgsubcl  16821  mulgdir  16832  issubg2  16881  issubgrpd2  16882  cycsubgcl  16892  cycsubgss  16893  nmzsubg  16907  eqgen  16919  ghmmulg  16944  conjghm  16962  symgfixfo  17129  odeq  17248  odval2  17249  odf1  17262  dfod2  17264  gexdvds  17284  gexdvds2  17286  gexcl2  17290  gexdvds3  17291  sylow2blem2  17322  efgsp1  17436  efgrelexlemb  17449  mulgmhm  17517  mulgghm  17518  iscyggen2  17565  iscyg3  17570  srglmhm  17817  srgrmhm  17818  ringlghm  17881  ringrghm  17882  gsumdixp  17886  dvdsrcl2  17927  crngunit  17939  kerf1hrm  18020  subrgugrp  18076  cntzsubr  18089  lmodvsdir  18164  lmodvsass  18165  lmodvsghm  18198  lsssubg  18229  lss1d  18235  islbs2  18426  lidlsubg  18487  lidlsubcl  18488  quscrng  18513  lpigen  18529  xrsdsreval  19062  expghm  19116  mulgghm2  19117  ip0r  19253  obs2ss  19341  islindf3  19433  scmatscm  19587  scmataddcl  19590  scmatsubcl  19591  scmatfo  19604  matunit  19752  cpmatelimp  19785  cpmatelimp2  19787  cpmatinvcl  19790  cpmatmcl  19792  mat2pmatf  19801  m2cpmf  19815  cpm2mf  19825  m2cpmfo  19829  m2cpminv  19833  decpmataa0  19841  pm2mpf  19871  pm2mpf1  19872  idpm2idmp  19874  pm2mpfo  19887  elcls2  20139  opnnei  20185  innei  20190  iscnp4  20328  cnpnei  20329  iscncl  20334  cnnei  20347  cnconst  20349  ordthauslem  20448  bwth  20474  1stccnp  20526  llyrest  20549  nllyrest  20550  kgenss  20607  xkoccn  20683  kqsat  20795  kqt0lem  20800  isr0  20801  fbssfi  20901  isfild  20922  filcon  20947  trfilss  20953  fgtr  20954  ufileu  20983  ufilen  20994  fmfnfmlem4  21021  fmfnfm  21022  hausflimi  21044  cnpflf2  21064  cnpflf  21065  cnflf  21066  cnpfcf  21105  cnfcf  21106  cnextcn  21131  tmdmulg  21156  clsnsg  21173  tsmsxplem1  21216  tsmsxp  21218  trust  21293  ustuqtop0  21304  ismeti  21389  isxmet2d  21391  elbl2ps  21453  elbl2  21454  xblpnfps  21459  xblpnf  21460  xbln0  21478  blin  21485  blssexps  21490  blssex  21491  blsscls2  21568  blcls  21570  blsscls  21571  metss  21572  metrest  21588  metcn  21607  metustbl  21630  psmetutop  21631  nmf2  21656  nmdvr  21722  nmoi  21782  nmoix  21783  nmoleub  21785  nmoiOLD  21798  nmoixOLD  21799  nmoleubOLD  21801  nghmcn  21815  xrsxmet  21876  iccntr  21888  metdsle  21918  metdsleOLD  21933  icoopnst  22016  iocopnst  22017  icccvx  22027  pi1xfr  22135  lmmbr  22277  lmmbr2  22278  iscfil3  22292  iscau2  22296  cfilres  22315  bcthlem1  22341  bcthlem4  22344  bcthlem5  22345  rrxmet  22411  ioombl  22567  iccvolcl  22569  ioovolcl  22571  mbfi1fseqlem3  22724  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  ig1pcl  23176  ig1prsp  23178  ig1pclOLD  23182  ig1prspOLD  23184  aannenlem1  23333  taylplem1  23367  dvtaylp  23374  relogeftb  23583  logdivlt  23619  cxpexp  23662  rpcxpcl  23670  isppw2  24091  vmappw  24092  lgslem4  24276  lgscllem  24280  lgsneg1  24297  lgsne0  24310  cgraswap  24911  brbtwn2  24984  ax5seglem1  25007  ax5seglem2  25008  axcontlem4  25046  nbgraf1olem5  25222  constr3cycl  25438  wwlknimp  25464  usg2wlkeq  25485  wwlknred  25500  wwlknext  25501  clwwlknprop  25549  3cyclfrgrarn1  25789  3cyclfrgrarn  25790  4cycl2vnunb  25794  frgrancvvdeqlemB  25815  usgreghash2spotv  25843  2spotmdisj  25845  grpoidinvlem3  25983  isvci  26250  nmcvcn  26380  ipval2lem2  26389  ipval2lem5  26395  sspival  26426  sspimsval  26428  isblo2  26473  nmoo0  26481  blocni  26495  isph  26512  sspph  26545  hvadd4  26738  hiassdi  26793  ocsh  26985  chj4  27237  spansncol  27270  pjjsi  27402  hoscl  27447  hodcl  27449  hoadd4  27486  homco1  27503  homulass  27504  hoadddi  27505  hoadddir  27506  unoplin  27622  adjvalval  27639  hmoplin  27644  bralnfn  27650  brafnmul  27653  lnopmi  27702  lnopcoi  27705  hmops  27722  hmopm  27723  nmophmi  27733  lnfncnbd  27759  cnlnadjlem2  27770  adjlnop  27788  adjmul  27794  adjadd  27795  branmfn  27807  kbass5  27822  kbass6  27823  leop2  27826  leopadd  27834  leopmuli  27835  pjimai  27878  atcvatlem  28087  chirredlem2  28093  mdsymlem3  28107  mdsymlem5  28109  sumdmdii  28117  sumdmdlem  28120  cdj3lem2a  28138  cdj3lem2b  28139  cdj3lem3a  28141  cdj3i  28143  xreceu  28440  toslublem  28477  tosglblem  28479  ogrpaddltbi  28531  archiabllem1b  28558  archiabllem2c  28561  archiabl  28564  slmdvsdir  28581  slmdvsass  28582  pstmxmet  28749  ordtconlem1  28779  hasheuni  28955  omsf  29169  omsfOLD  29173  ballotlemirc  29413  ballotlemircOLD  29451  signswmnd  29495  bnj1204  29870  txpcon  30004  cvmscld  30045  elmpps  30260  dfrdg2  30491  wsuclem  30557  nobndlem8  30637  segconeu  30827  linecom  30966  linethru  30969  lineintmo  30973  fnemeet2  31072  fnejoin2  31074  heicant  32020  mblfinlem1  32022  mblfinlem3  32024  ismblfin  32026  cnambfre  32034  itg2addnclem2  32039  ftc1anclem1  32062  ftc1anclem5  32066  ftc1anclem6  32067  ftc2nc  32071  areacirclem2  32078  areacirclem4  32080  areacirclem5  32081  areacirc  32082  fzmul  32114  subspopn  32126  isbndx  32159  isbnd2  32160  isbnd3  32161  ssbnd  32165  prdstotbnd  32171  heibor1  32187  rrnmet  32206  rngonegmn1l  32233  rngohomco  32258  rngoisocnv  32265  rngoisoco  32266  crngohomfo  32284  isidlc  32293  rngoidl  32302  prnc  32345  ispridlc  32348  cvrval2  32885  glbconxN  32988  hlrelat5N  33011  cvratlem  33031  cvrat2  33039  athgt  33066  3dim2  33078  llnn0  33126  lplnn0N  33157  lvoln0N  33201  snatpsubN  33360  paddasslem18  33447  pmod1i  33458  lhpexle2  33620  lhpexle3lem  33621  lhpexle3  33622  ldilcnv  33725  trlcnv  33776  trlnidatb  33788  cdleme32snaw  34047  cdleme32fvaw  34051  cdleme42ke  34097  cdlemeg46gf  34145  cdleme50trn12  34164  cdlemg1cex  34200  cdlemb3  34218  tgrpgrplem  34361  tgrpabl  34363  tendoplcl2  34390  tendo0pl  34403  tendoicl  34408  tendoipl  34409  cdlemkid3N  34545  tendoex  34587  erngdvlem4  34603  erngdvlem4-rN  34611  dib1dim  34778  dib1dim2  34781  dihglbcpreN  34913  dihmeetALTN  34940  dih1dimatlem  34942  dihatlat  34947  oddcomabszz  35837  acongtr  35873  rpnnen3lem  35931  islssfg  35973  lmhmfgsplit  35989  unxpwdom3  35998  hbtlem7  36029  sdrgacs  36112  hashgcdeq  36120  iocmbl  36142  ss2iundf  36296  nzss  36710  dvconstbi  36727  bccbc  36738  uzmptshftfval  36739  iccdifprioo  37655  dvnmul  37856  fourierdlem74  38082  fourierdlem75  38083  issald  38230  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0iunmpt  38298  sge0xp  38309  volico  38401  hspmbllem2  38487  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  pfxccat1  38991  ralxfrd2  39048  vtxdgfisf  39586  ewlkprop  39670  uhgr1wlkspthlem2  39786  usgra2pthlem1  39940  rnghmsubcsetclem2  40251  rhmsubcsetclem2  40297  rhmsubcrngclem2  40303  lcoss  40502  snlindsntorlem  40536  aacllem  40813
  Copyright terms: Public domain W3C validator