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

Theorem 3expa 1194
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 1193 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 430 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  3anidm23  1285  mp3an2  1310  mpd3an3  1323  rgen3  2808  moi2  3205  sbc3ie  3322  2if2  3905  preq12bg  4123  prel12g  4124  reuhypd  4589  otsndisj  4666  fvtp1g  6023  f1imass  6073  weisoeq  6152  f1ofveu  6191  f1ocnvfv3  6192  curry1f  6793  curry2f  6795  funsssuppss  6844  tfrlem11  6975  oalimcl  7127  oeordsuc  7161  oelim2  7162  nneob  7219  mapxpen  7602  findcard  7674  wemaplem3  7888  en2eqpr  8298  infxpabs  8505  infxp  8508  cfflb  8552  cfsmolem  8563  isf32lem12  8657  fin1a2lem9  8701  fin1a2s  8707  axcc3  8731  axdc3lem4  8746  zornn0g  8798  pwfseqlem4  8951  tskwun  9073  tskint  9074  tskxp  9076  tskmap  9077  gruf  9100  gruwun  9102  grutsk1  9110  addcanpi  9188  ltapi  9192  mul4  9660  add4  9707  2addsub  9747  addsubeq4  9748  muladd  9907  ltleadd  9953  receu  10111  p1le  10302  lemul12b  10316  lbinfm  10412  zdiv  10850  fzind  10877  fnn0ind  10878  uzss  11021  zbtwnre  11099  qmulcl  11119  qreccl  11121  xrlttr  11267  xaddass  11362  xmulasslem3  11399  xmulass  11400  xadddilem  11407  xrsupsslem  11419  xrinfmsslem  11420  supxrunb1  11432  ixxin  11467  ioo0  11475  ico0  11496  ioc0  11497  icc0  11498  iooshf  11524  prunioo  11570  ioojoin  11572  elfz5  11601  elfz0fzfz0  11701  elfzonelfzo  11811  fzind2  11823  mulexpz  12109  expsub  12116  digit2  12201  digit1  12202  facndiv  12268  faclbnd4lem4  12276  faclbnd4  12277  faclbnd5  12278  bccmpl  12289  bcval5  12298  bcpasc  12301  hashunx  12357  ccatrn  12515  swrdccat1  12593  swrdccat2  12594  swrdswrd  12596  cats1un  12612  crim  12950  absmax  13164  ello12r  13342  elo12r  13353  climshftlem  13399  2sumeq2dv  13529  expcnv  13677  2cprodeq2dv  13734  rpnnen2lem7  13956  dvdsval3  13992  dvdsnegb  14003  muldvds1  14010  muldvds2  14011  dvdscmul  14012  dvdsmulc  14013  dvdsmulcr  14015  dvds2ln  14016  divalgb  14064  ndvdssub  14067  gcddiv  14189  rpexp1i  14264  phiprmpw  14308  pythagtriplem1  14342  pockthg  14426  infpnlem1  14430  4sqlem3  14470  0ramcl  14543  firest  14840  imasaddfnlem  14935  imasleval  14948  xpsfrn2  14977  mrerintcl  15004  iscatd  15080  fullestrcsetc  15537  fullsetcestrc  15552  clatleglb  15873  mreclatBAD  15934  pslem  15953  mrcmndind  16114  grplmulf1o  16229  grplactcnv  16255  mulgnn0subcl  16272  mulgsubcl  16273  mulgdir  16284  issubg2  16333  issubgrpd2  16334  cycsubgcl  16344  cycsubgss  16345  nmzsubg  16359  eqgen  16371  ghmmulg  16396  conjghm  16414  symgfixfo  16581  odeq  16691  odval2  16692  odf1  16701  dfod2  16703  gexdvds  16721  gexdvds2  16722  gexcl2  16726  gexdvds3  16727  sylow2blem2  16758  efgsp1  16872  efgrelexlemb  16885  mulgmhm  16953  mulgghm  16954  iscyggen2  17001  iscyg3  17006  srglmhm  17299  srgrmhm  17300  ringlghm  17363  ringrghm  17364  gsumdixpOLD  17370  gsumdixp  17371  dvdsrcl2  17412  crngunit  17424  kerf1hrm  17505  subrgugrp  17561  cntzsubr  17574  lmodvsdir  17649  lmodvsass  17650  lmodvsghm  17684  lsssubg  17716  lss1d  17722  islbs2  17913  lidlsubg  17975  lidlsubcl  17976  quscrng  18001  lpigen  18017  xrsdsreval  18576  expghm  18626  mulgghm2  18627  ip0r  18763  obs2ss  18851  islindf3  18946  scmatscm  19100  scmataddcl  19103  scmatsubcl  19104  scmatfo  19117  matunit  19265  cpmatelimp  19298  cpmatelimp2  19300  cpmatinvcl  19303  cpmatmcl  19305  mat2pmatf  19314  m2cpmf  19328  cpm2mf  19338  m2cpmfo  19342  m2cpminv  19346  decpmataa0  19354  pm2mpf  19384  pm2mpf1  19385  idpm2idmp  19387  pm2mpfo  19400  elcls2  19661  opnnei  19707  innei  19712  iscnp4  19850  cnpnei  19851  iscncl  19856  cnnei  19869  cnconst  19871  ordthauslem  19970  bwth  19996  1stccnp  20048  llyrest  20071  nllyrest  20072  kgenss  20129  xkoccn  20205  kqsat  20317  kqt0lem  20322  isr0  20323  fbssfi  20423  isfild  20444  filcon  20469  trfilss  20475  fgtr  20476  ufileu  20505  ufilen  20516  fmfnfmlem4  20543  fmfnfm  20544  hausflimi  20566  cnpflf2  20586  cnpflf  20587  cnflf  20588  cnpfcf  20627  cnfcf  20628  cnextcn  20652  tmdmulg  20676  clsnsg  20693  tsmsxplem1  20740  tsmsxp  20742  trust  20817  ustuqtop0  20828  ismeti  20913  isxmet2d  20915  elbl2ps  20977  elbl2  20978  xblpnfps  20983  xblpnf  20984  xbln0  21002  blin  21009  blssexps  21014  blssex  21015  blsscls2  21092  blcls  21094  blsscls  21095  metss  21096  metrest  21112  metcn  21131  metustblOLD  21168  metustbl  21169  metutopOLD  21170  psmetutop  21171  nmf2  21198  nmdvr  21264  nmoi  21320  nmoix  21321  nmoleub  21323  nghmcn  21337  xrsxmet  21399  iccntr  21411  metdsle  21441  icoopnst  21524  iocopnst  21525  icccvx  21535  pi1xfr  21640  lmmbr  21782  lmmbr2  21783  iscfil3  21797  iscau2  21801  cfilres  21820  bcthlem1  21848  bcthlem4  21851  bcthlem5  21852  rrxmet  21920  ioombl  22060  iccvolcl  22062  ioovolcl  22064  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  ig1pcl  22661  ig1prsp  22663  aannenlem1  22809  taylplem1  22843  dvtaylp  22850  relogeftb  23057  logdivlt  23093  cxpexp  23136  rpcxpcl  23144  isppw2  23506  vmappw  23507  lgslem4  23691  lgscllem  23695  lgsneg1  23712  lgsne0  23725  brbtwn2  24329  ax5seglem1  24352  ax5seglem2  24353  axcontlem4  24391  nbgraf1olem5  24566  constr3cycl  24782  wwlknimp  24808  usg2wlkeq  24829  wwlknred  24844  wwlknext  24845  clwwlknprop  24893  3cyclfrgrarn1  25133  3cyclfrgrarn  25134  4cycl2vnunb  25138  frgrancvvdeqlemB  25159  usgreghash2spotv  25187  2spotmdisj  25189  grpoidinvlem3  25325  isvci  25592  nmcvcn  25722  ipval2lem2  25731  ipval2lem5  25737  sspival  25768  sspimsval  25770  isblo2  25815  nmoo0  25823  blocni  25837  isph  25854  sspph  25887  hvadd4  26070  hiassdi  26125  ocsh  26318  chj4  26570  spansncol  26603  pjjsi  26735  hoscl  26780  hodcl  26782  hoadd4  26819  homco1  26836  homulass  26837  hoadddi  26838  hoadddir  26839  unoplin  26955  adjvalval  26972  hmoplin  26977  bralnfn  26983  brafnmul  26986  lnopmi  27035  lnopcoi  27038  hmops  27055  hmopm  27056  nmophmi  27066  lnfncnbd  27092  cnlnadjlem2  27103  adjlnop  27121  adjmul  27127  adjadd  27128  branmfn  27140  kbass5  27155  kbass6  27156  leop2  27159  leopadd  27167  leopmuli  27168  pjimai  27211  atcvatlem  27420  chirredlem2  27426  mdsymlem3  27440  mdsymlem5  27442  sumdmdii  27450  sumdmdlem  27453  cdj3lem2a  27471  cdj3lem2b  27472  cdj3lem3a  27474  cdj3i  27476  xreceu  27771  toslublem  27808  tosglblem  27810  ogrpaddltbi  27862  archiabllem1b  27889  archiabllem2c  27892  archiabl  27895  slmdvsdir  27912  slmdvsass  27913  pstmxmet  28030  ordtconlem1  28060  hasheuni  28233  omsf  28423  ballotlemirc  28653  signswmnd  28697  txpcon  28866  cvmscld  28907  elmpps  29122  dfrdg2  29393  wsuclem  29546  nobndlem8  29624  segconeu  29814  linecom  29953  linethru  29956  lineintmo  29960  heicant  30214  mblfinlem1  30216  mblfinlem3  30218  ismblfin  30220  cnambfre  30228  itg2addnclem2  30233  ftc1anclem1  30256  ftc1anclem5  30260  ftc1anclem6  30261  ftc2nc  30265  areacirclem2  30274  areacirclem4  30276  areacirclem5  30277  areacirc  30278  fnemeet2  30351  fnejoin2  30353  fzmul  30399  subspopn  30411  isbndx  30444  isbnd2  30445  isbnd3  30446  ssbnd  30450  prdstotbnd  30456  heibor1  30472  rrnmet  30491  rngonegmn1l  30518  rngohomco  30543  rngoisocnv  30550  rngoisoco  30551  crngohomfo  30569  isidlc  30578  rngoidl  30587  prnc  30630  ispridlc  30633  oddcomabszz  31045  acongtr  31081  rpnnen3lem  31139  islssfg  31182  lmhmfgsplit  31198  unxpwdom3  31207  hbtlem7  31242  sdrgacs  31318  hashgcdeq  31326  iocmbl  31348  nzss  31390  dvconstbi  31407  bccbc  31418  uzmptshftfval  31419  iccdifprioo  31722  dvnmul  31906  fourierdlem74  32129  fourierdlem75  32130  pfxccat1  32585  ralxfrd2  32624  usgra2pthlem1  32671  rnghmsubcsetclem2  32984  rhmsubcsetclem2  33030  rhmsubcrngclem2  33036  lcoss  33237  snlindsntorlem  33271  aacllem  33550  bnj1204  34415  cvrval2  35412  glbconxN  35515  hlrelat5N  35538  cvratlem  35558  cvrat2  35566  athgt  35593  3dim2  35605  llnn0  35653  lplnn0N  35684  lvoln0N  35728  snatpsubN  35887  paddasslem18  35974  pmod1i  35985  lhpexle2  36147  lhpexle3lem  36148  lhpexle3  36149  ldilcnv  36252  trlcnv  36303  trlnidatb  36315  cdleme32snaw  36574  cdleme32fvaw  36578  cdleme42ke  36624  cdlemeg46gf  36672  cdleme50trn12  36691  cdlemg1cex  36727  cdlemb3  36745  tgrpgrplem  36888  tgrpabl  36890  tendoplcl2  36917  tendo0pl  36930  tendoicl  36935  tendoipl  36936  cdlemkid3N  37072  tendoex  37114  erngdvlem4  37130  erngdvlem4-rN  37138  dib1dim  37305  dib1dim2  37308  dihglbcpreN  37440  dihmeetALTN  37467  dih1dimatlem  37469  dihatlat  37474
  Copyright terms: Public domain W3C validator