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

Theorem 3expa 1153
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 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anidm23  1243  mp3an2  1267  mpd3an3  1280  rgen3  2790  moi2  3102  sbc3ie  3217  preq12bg  3964  reuhypd  4736  fvtp1g  5928  f1imass  5996  fcof1o  6012  weisoeq  6062  curry1f  6426  curry2f  6428  riota5OLD  6562  f1ofveu  6570  f1ocnvfv3  6571  tfrlem11  6635  oalimcl  6789  oeordsuc  6823  oelim2  6824  nneob  6881  mapxpen  7259  findcard  7333  wemaplem3  7501  en2eqpr  7875  infxpabs  8076  infxp  8079  cfflb  8123  cfsmolem  8134  isf32lem12  8228  fin1a2lem9  8272  fin1a2s  8278  axcc3  8302  axdc3lem4  8317  zornn0g  8369  pwfseqlem4  8521  tskwun  8643  tskint  8644  tskxp  8646  tskmap  8647  gruf  8670  gruwun  8672  grutsk1  8680  addcanpi  8760  ltapi  8764  mul4  9219  add4  9265  2addsub  9303  addsubeq4  9304  muladd  9450  ltleadd  9495  receu  9651  p1le  9837  lemul12b  9851  lbinfm  9945  zdiv  10324  fzind  10352  fnn0ind  10353  uzss  10490  zbtwnre  10556  qmulcl  10576  qreccl  10578  xrlttr  10717  xaddass  10812  xmulasslem3  10849  xmulass  10850  xadddilem  10857  xrsupsslem  10869  xrinfmsslem  10870  supxrunb1  10882  ixxin  10917  ioo0  10925  ico0  10946  ioc0  10947  icc0  10948  iooshf  10973  prunioo  11009  ioojoin  11011  elfz5  11035  fzind2  11181  mulexpz  11403  expsub  11410  digit2  11495  digit1  11496  facndiv  11562  faclbnd4lem4  11570  faclbnd4  11571  faclbnd5  11572  bccmpl  11583  bcval5  11592  bcpasc  11595  hashunx  11643  swrdccat1  11757  swrdccat2  11758  cats1un  11773  crim  11903  absmax  12116  ello12r  12294  elo12r  12305  climshftlem  12351  2sumeq2dv  12482  expcnv  12626  rpnnen2lem7  12803  dvdsval3  12839  dvdsnegb  12850  muldvds1  12857  muldvds2  12858  dvdscmul  12859  dvdsmulc  12860  dvdsmulcr  12862  dvds2ln  12863  divalgb  12907  ndvdssub  12910  gcddiv  13032  rpexp1i  13104  phiprmpw  13148  pythagtriplem1  13173  pockthg  13257  infpnlem1  13261  4sqlem3  13301  0ramcl  13374  firest  13643  imasaddfnlem  13736  imasleval  13749  xpsfrn2  13778  mrerintcl  13805  iscatd  13881  lubid  14422  clatleglb  14536  mreclat  14596  pslem  14621  grplmulf1o  14848  grplactcnv  14870  mulgnn0subcl  14886  mulgsubcl  14887  mulgdir  14898  issubg2  14942  cycsubgcl  14949  cycsubgss  14950  nmzsubg  14964  eqgen  14976  ghmmulg  15001  conjghm  15019  odeq  15171  odval2  15172  odf1  15181  dfod2  15183  gexdvds  15201  gexdvds2  15202  gexcl2  15206  gexdvds3  15207  sylow2blem2  15238  efgsp1  15352  efgrelexlemb  15365  mulgmhm  15433  mulgghm  15434  iscyggen2  15474  iscyg3  15479  rnglghm  15694  rngrghm  15695  gsumdixp  15698  dvdsrcl2  15738  crngunit  15750  subrgugrp  15870  cntzsubr  15883  lmodvsdir  15957  lmodvsass  15958  lmodvsghm  15988  lsssubg  16016  lss1d  16022  islbs2  16209  issubgrpd2  16243  lidlsubg  16269  divscrng  16294  lpigen  16310  xrsdsreval  16726  expghm  16760  mulgghm2  16769  ip0r  16851  obs2ss  16939  elcls2  17121  opnnei  17167  innei  17172  iscnp4  17310  cnpnei  17311  iscncl  17316  cnnei  17329  cnconst  17331  ordthauslem  17430  1stccnp  17508  llyrest  17531  nllyrest  17532  kgenss  17558  xkoccn  17634  kqsat  17746  kqt0lem  17751  isr0  17752  fbssfi  17852  isfild  17873  filcon  17898  trfilss  17904  fgtr  17905  ufileu  17934  ufilen  17945  fmfnfmlem4  17972  fmfnfm  17973  hausflimi  17995  cnpflf2  18015  cnpflf  18016  cnflf  18017  cnpfcf  18056  cnfcf  18057  cnextcn  18081  tmdmulg  18105  clsnsg  18122  tsmsxplem1  18165  tsmsxp  18167  trust  18242  ustuqtop0  18253  ismeti  18338  isxmet2d  18340  elbl2ps  18402  elbl2  18403  xblpnfps  18408  xblpnf  18409  xbln0  18427  blin  18434  blssexps  18439  blssex  18440  blsscls2  18517  blcls  18519  blsscls  18520  metss  18521  metrest  18537  metcn  18556  metustblOLD  18593  metustbl  18594  metutopOLD  18595  psmetutop  18596  nmf2  18623  nmdvr  18689  nmoi  18745  nmoix  18746  nmoleub  18748  nghmcn  18762  xrsxmet  18823  iccntr  18835  metdsle  18865  icoopnst  18947  iocopnst  18948  icccvx  18958  pi1xfr  19063  lmmbr  19194  lmmbr2  19195  iscfil3  19209  iscau2  19213  cfilres  19232  bcthlem1  19260  bcthlem4  19263  bcthlem5  19264  ioombl  19442  iccvolcl  19444  mbfi1fseqlem3  19592  mbfi1fseqlem4  19593  mbfi1fseqlem5  19594  ig1pcl  20081  ig1prsp  20083  aannenlem1  20228  taylplem1  20262  dvtaylp  20269  relogeftb  20462  logdivlt  20499  cxpexp  20542  rpcxpcl  20550  isppw2  20881  vmappw  20882  lgslem4  21066  lgscllem  21070  lgsneg1  21087  lgsne0  21100  nbgraf1olem5  21438  constr3cycl  21631  grpoidinvlem3  21777  isvci  22044  nmcvcn  22174  ipval2lem2  22183  ipval2lem5  22189  sspival  22220  sspimsval  22222  isblo2  22267  nmoo0  22275  blocni  22289  isph  22306  sspph  22339  hvadd4  22521  hiassdi  22576  ocsh  22768  chj4  23020  spansncol  23053  pjjsi  23185  hoscl  23231  hodcl  23233  hoadd4  23270  homco1  23287  homulass  23288  hoadddi  23289  hoadddir  23290  unoplin  23406  adjvalval  23423  hmoplin  23428  bralnfn  23434  brafnmul  23437  lnopmi  23486  lnopcoi  23489  hmops  23506  hmopm  23507  nmophmi  23517  lnfncnbd  23543  cnlnadjlem2  23554  adjlnop  23572  adjmul  23578  adjadd  23579  branmfn  23591  kbass5  23606  kbass6  23607  leop2  23610  leopadd  23618  leopmuli  23619  pjimai  23662  atcvatlem  23871  chirredlem2  23877  mdsymlem3  23891  mdsymlem5  23893  sumdmdii  23901  sumdmdlem  23904  cdj3lem2a  23922  cdj3lem2b  23923  cdj3lem3a  23925  cdj3i  23927  xreceu  24151  toslub  24174  tosglb  24175  xrstos  24184  hasheuni  24458  ballotlemirc  24772  txpcon  24902  cvmscld  24943  2cprodeq2dv  25235  dfrdg2  25402  nobndlem8  25603  brbtwn2  25787  ax5seglem1  25810  ax5seglem2  25811  axcontlem4  25849  segconeu  25888  linecom  26027  linethru  26030  lineintmo  26034  mblfinlem  26185  mblfinlem2  26186  ismblfin  26188  cnambfre  26196  itg2addnclem2  26198  areacirclem4  26225  areacirclem5  26227  areacirclem6  26228  areacirc  26229  fnemeet2  26328  fnejoin2  26330  fzmul  26376  subspopn  26390  isbndx  26423  isbnd2  26424  isbnd3  26425  ssbnd  26429  prdstotbnd  26435  heibor1  26451  rrnmet  26470  rngonegmn1l  26497  rngohomco  26522  rngoisocnv  26529  rngoisoco  26530  crngohomfo  26548  isidlc  26557  rngoidl  26566  prnc  26609  ispridlc  26612  oddcomabszz  26939  acongtr  26975  rpnnen3lem  27034  islssfg  27078  lmhmfgsplit  27094  unxpwdom3  27166  islindf3  27206  hbtlem7  27239  sdrgacs  27419  hashgcdeq  27427  dvconstbi  27461  ioovolcl  27651  2if2  27983  otsndisj  27995  elfzonelfzo  28034  swrdswrd  28053  usgra2pthlem1  28082  3cyclfrgrarn1  28158  3cyclfrgrarn  28159  4cycl2vnunb  28163  frgrancvvdeqlemB  28183  usgreghash2spotv  28211  2spotmdisj  28213  bnj1204  29133  cvrval2  29803  glbconxN  29906  hlrelat5N  29929  cvratlem  29949  cvrat2  29957  athgt  29984  3dim2  29996  llnn0  30044  lplnn0N  30075  lvoln0N  30119  snatpsubN  30278  paddasslem18  30365  pmod1i  30376  lhpexle2  30538  lhpexle3lem  30539  lhpexle3  30540  ldilcnv  30643  trlcnv  30693  trlnidatb  30705  cdleme32snaw  30963  cdleme32fvaw  30967  cdleme42ke  31013  cdlemeg46gf  31061  cdleme50trn12  31080  cdlemg1cex  31116  cdlemb3  31134  tgrpgrplem  31277  tgrpabl  31279  tendoplcl2  31306  tendo0pl  31319  tendoicl  31324  tendoipl  31325  cdlemkid3N  31461  tendoex  31503  erngdvlem4  31519  erngdvlem4-rN  31527  dib1dim  31694  dib1dim2  31697  dihglbcpreN  31829  dihmeetALTN  31856  dih1dimatlem  31858  dihatlat  31863
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator