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

Theorem 3expa 1151
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 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anidm23  1241  mp3an2  1265  mpd3an3  1278  rgen3  2653  moi2  2959  sbc3ie  3073  preq12bg  3807  reuhypd  4577  f1imass  5804  fcof1o  5819  weisoeq  5869  curry1f  6228  curry2f  6230  riota5OLD  6347  f1ofveu  6355  f1ocnvfv3  6356  tfrlem11  6420  oalimcl  6574  oeordsuc  6608  oelim2  6609  nneob  6666  mapxpen  7043  findcard  7113  wemaplem3  7279  en2eqpr  7653  infxpabs  7854  infxp  7857  cfflb  7901  cfsmolem  7912  isf32lem12  8006  fin1a2lem9  8050  fin1a2s  8056  axcc3  8080  axdc3lem4  8095  zornn0g  8148  pwfseqlem4  8300  tskwun  8422  tskint  8423  tskxp  8425  tskmap  8426  gruf  8449  gruwun  8451  grutsk1  8459  addcanpi  8539  ltapi  8543  mul4  8997  add4  9043  2addsub  9081  addsubeq4  9082  muladd  9228  ltleadd  9273  receu  9429  p1le  9615  lemul12b  9629  lbinfm  9723  zdiv  10098  fzind  10126  fnn0ind  10127  uzss  10264  zbtwnre  10330  qmulcl  10350  qreccl  10352  xrlttr  10490  xaddass  10585  xmulasslem3  10622  xmulass  10623  xadddilem  10630  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  ixxin  10689  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  iooshf  10744  prunioo  10780  ioojoin  10782  elfz5  10806  fzind2  10939  mulexpz  11158  expsub  11165  digit2  11250  digit1  11251  facndiv  11317  faclbnd4lem4  11325  faclbnd4  11326  faclbnd5  11327  bccmpl  11338  bcval5  11346  bcpasc  11349  swrdccat1  11476  swrdccat2  11477  cats1un  11492  crim  11616  absmax  11829  ello12r  12007  elo12r  12018  climshftlem  12064  2sumeq2dv  12194  expcnv  12338  rpnnen2lem7  12515  dvdsval3  12551  dvdsnegb  12562  muldvds1  12569  muldvds2  12570  dvdscmul  12571  dvdsmulc  12572  dvdsmulcr  12574  dvds2ln  12575  divalgb  12619  ndvdssub  12622  gcddiv  12744  rpexp1i  12816  phiprmpw  12860  pythagtriplem1  12885  pockthg  12969  infpnlem1  12973  4sqlem3  13013  0ramcl  13086  firest  13353  imasaddfnlem  13446  imasleval  13459  xpsfrn2  13488  mrerintcl  13515  iscatd  13591  lubid  14132  clatleglb  14246  mreclat  14306  pslem  14331  grplmulf1o  14558  grplactcnv  14580  mulgnn0subcl  14596  mulgsubcl  14597  mulgdir  14608  issubg2  14652  cycsubgcl  14659  cycsubgss  14660  nmzsubg  14674  eqgen  14686  ghmmulg  14711  conjghm  14729  odeq  14881  odval2  14882  odf1  14891  dfod2  14893  gexdvds  14911  gexdvds2  14912  gexcl2  14916  gexdvds3  14917  sylow2blem2  14948  efgsp1  15062  efgrelexlemb  15075  mulgmhm  15143  mulgghm  15144  iscyggen2  15184  iscyg3  15189  rnglghm  15404  rngrghm  15405  gsumdixp  15408  dvdsrcl2  15448  crngunit  15460  subrgugrp  15580  cntzsubr  15593  lmodvsdir  15668  lmodvsass  15670  lmodvsghm  15702  lsssubg  15730  lss1d  15736  islbs2  15923  issubgrpd2  15957  lidlsubg  15983  divscrng  16008  lpigen  16024  xrsdsreval  16432  expghm  16466  mulgghm2  16475  ip0r  16557  obs2ss  16645  elcls2  16827  opnnei  16873  innei  16878  cnpnei  17009  iscncl  17014  cnconst  17028  ordthauslem  17127  1stccnp  17204  llyrest  17227  nllyrest  17228  kgenss  17254  xkoccn  17329  kqsat  17438  kqt0lem  17443  isr0  17444  fbssfi  17548  isfild  17569  filcon  17594  trfilss  17600  fgtr  17601  ufileu  17630  ufilen  17641  fmfnfmlem4  17668  fmfnfm  17669  hausflimi  17691  cnpflf2  17711  cnpflf  17712  cnflf  17713  cnpfcf  17752  cnfcf  17753  tmdmulg  17791  clsnsg  17808  tsmsxplem1  17851  tsmsxp  17853  ismeti  17906  isxmet2d  17908  elbl2  17966  xblpnf  17969  xbln0  17981  blin  17986  blssex  17989  blsscls2  18066  blcls  18068  blsscls  18069  metss  18070  metrest  18086  metcn  18105  nmf2  18131  nmdvr  18197  nmoi  18253  nmoix  18254  nmoleub  18256  nghmcn  18270  xrsxmet  18331  iccntr  18342  metdsle  18372  icoopnst  18453  iocopnst  18454  icccvx  18464  pi1xfr  18569  lmmbr  18700  lmmbr2  18701  iscfil3  18715  iscau2  18719  cfilres  18738  bcthlem1  18762  bcthlem4  18765  bcthlem5  18766  ioombl  18938  iccvolcl  18940  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  dvmptfsum  19338  ig1pcl  19577  ig1prsp  19579  aannenlem1  19724  taylplem1  19758  dvtaylp  19765  relogeftb  19954  logdivlt  19988  cxpexp  20031  rpcxpcl  20039  isppw2  20369  vmappw  20370  lgslem4  20554  lgscllem  20558  lgsneg1  20575  lgsne0  20588  grpoidinvlem3  20889  isvci  21154  nmcvcn  21284  ipval2lem2  21293  ipval2lem5  21299  sspival  21330  sspimsval  21332  isblo2  21377  nmoo0  21385  blocni  21399  isph  21416  sspph  21449  hvadd4  21631  hiassdi  21686  ocsh  21878  chj4  22130  spansncol  22163  pjjsi  22295  hoscl  22341  hodcl  22343  hoadd4  22380  homco1  22397  homulass  22398  hoadddi  22399  hoadddir  22400  unoplin  22516  adjvalval  22533  hmoplin  22538  bralnfn  22544  brafnmul  22547  lnopmi  22596  lnopcoi  22599  hmops  22616  hmopm  22617  nmophmi  22627  lnfncnbd  22653  cnlnadjlem2  22664  adjlnop  22682  adjmul  22688  adjadd  22689  branmfn  22701  kbass5  22716  kbass6  22717  leop2  22720  leopadd  22728  leopmuli  22729  pjimai  22772  atcvatlem  22981  chirredlem2  22987  mdsymlem3  23001  mdsymlem5  23003  sumdmdii  23011  sumdmdlem  23014  cdj3lem2a  23032  cdj3lem2b  23033  cdj3lem3a  23035  cdj3i  23037  ballotlemirc  23106  xreceu  23121  abfmpeld  23233  abfmpel  23234  hasheuni  23468  txpcon  23778  cvmscld  23819  faclimlem5  24121  2cprodeq2dv  24147  dfrdg2  24223  nobndlem8  24424  brbtwn2  24605  ax5seglem1  24628  ax5seglem2  24629  axcontlem4  24667  segconeu  24706  linecom  24845  linethru  24848  lineintmo  24852  itg2addnclem2  25004  areacirclem4  25030  areacirclem5  25032  areacirclem6  25033  areacirc  25034  cmprtr  25499  cmpltr2  25510  cmperltr  25512  iscnp4  25666  cmp2morp  26061  cmpmor  26078  fnemeet2  26419  fnejoin2  26421  infmrlbOLD  26525  fzmul  26546  subspopn  26569  isbndx  26609  isbnd2  26610  isbnd3  26611  ssbnd  26615  prdstotbnd  26621  heibor1  26637  rrnmet  26656  rngonegmn1l  26683  rngohomco  26708  rngoisocnv  26715  rngoisoco  26716  crngohomfo  26734  isidlc  26743  rngoidl  26752  prnc  26795  ispridlc  26798  oddcomabszz  27132  acongtr  27168  rpnnen3lem  27227  islssfg  27271  lmhmfgsplit  27287  unxpwdom3  27359  islindf3  27399  hbtlem7  27432  sdrgacs  27612  hashgcdeq  27620  dvconstbi  27654  ioovolcl  27845  constr3cycl  28407  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  4cycl2vnunb  28439  bnj1204  29358  cvrval2  30086  glbconxN  30189  hlrelat5N  30212  cvratlem  30232  cvrat2  30240  athgt  30267  3dim2  30279  llnn0  30327  lplnn0N  30358  lvoln0N  30402  snatpsubN  30561  paddasslem18  30648  pmod1i  30659  lhpexle2  30821  lhpexle3lem  30822  lhpexle3  30823  ldilcnv  30926  trlcnv  30976  trlnidatb  30988  cdleme32snaw  31246  cdleme32fvaw  31250  cdleme42ke  31296  cdlemeg46gf  31344  cdleme50trn12  31363  cdlemg1cex  31399  cdlemb3  31417  tgrpgrplem  31560  tgrpabl  31562  tendoplcl2  31589  tendo0pl  31602  tendoicl  31607  tendoipl  31608  cdlemkid3N  31744  tendoex  31786  erngdvlem4  31802  erngdvlem4-rN  31810  dib1dim  31977  dib1dim2  31980  dihglbcpreN  32112  dihmeetALTN  32139  dih1dimatlem  32141  dihatlat  32146
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator