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

Theorem 3expa 1154
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 1153 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 423 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anidm23  1244  mp3an2  1268  mpd3an3  1281  rgen3  2805  moi2  3117  sbc3ie  3232  preq12bg  3979  reuhypd  4752  fvtp1g  5944  f1imass  6012  fcof1o  6028  weisoeq  6078  curry1f  6442  curry2f  6444  riota5OLD  6578  f1ofveu  6586  f1ocnvfv3  6587  tfrlem11  6651  oalimcl  6805  oeordsuc  6839  oelim2  6840  nneob  6897  mapxpen  7275  findcard  7349  wemaplem3  7519  en2eqpr  7893  infxpabs  8094  infxp  8097  cfflb  8141  cfsmolem  8152  isf32lem12  8246  fin1a2lem9  8290  fin1a2s  8296  axcc3  8320  axdc3lem4  8335  zornn0g  8387  pwfseqlem4  8539  tskwun  8661  tskint  8662  tskxp  8664  tskmap  8665  gruf  8688  gruwun  8690  grutsk1  8698  addcanpi  8778  ltapi  8782  mul4  9237  add4  9283  2addsub  9321  addsubeq4  9322  muladd  9468  ltleadd  9513  receu  9669  p1le  9855  lemul12b  9869  lbinfm  9963  zdiv  10342  fzind  10370  fnn0ind  10371  uzss  10508  zbtwnre  10574  qmulcl  10594  qreccl  10596  xrlttr  10735  xaddass  10830  xmulasslem3  10867  xmulass  10868  xadddilem  10875  xrsupsslem  10887  xrinfmsslem  10888  supxrunb1  10900  ixxin  10935  ioo0  10943  ico0  10964  ioc0  10965  icc0  10966  iooshf  10991  prunioo  11027  ioojoin  11029  elfz5  11053  fzind2  11200  mulexpz  11422  expsub  11429  digit2  11514  digit1  11515  facndiv  11581  faclbnd4lem4  11589  faclbnd4  11590  faclbnd5  11591  bccmpl  11602  bcval5  11611  bcpasc  11614  hashunx  11662  swrdccat1  11776  swrdccat2  11777  cats1un  11792  crim  11922  absmax  12135  ello12r  12313  elo12r  12324  climshftlem  12370  2sumeq2dv  12501  expcnv  12645  rpnnen2lem7  12822  dvdsval3  12858  dvdsnegb  12869  muldvds1  12876  muldvds2  12877  dvdscmul  12878  dvdsmulc  12879  dvdsmulcr  12881  dvds2ln  12882  divalgb  12926  ndvdssub  12929  gcddiv  13051  rpexp1i  13123  phiprmpw  13167  pythagtriplem1  13192  pockthg  13276  infpnlem1  13280  4sqlem3  13320  0ramcl  13393  firest  13662  imasaddfnlem  13755  imasleval  13768  xpsfrn2  13797  mrerintcl  13824  iscatd  13900  lubid  14441  clatleglb  14555  mreclat  14615  pslem  14640  grplmulf1o  14867  grplactcnv  14889  mulgnn0subcl  14905  mulgsubcl  14906  mulgdir  14917  issubg2  14961  cycsubgcl  14968  cycsubgss  14969  nmzsubg  14983  eqgen  14995  ghmmulg  15020  conjghm  15038  odeq  15190  odval2  15191  odf1  15200  dfod2  15202  gexdvds  15220  gexdvds2  15221  gexcl2  15225  gexdvds3  15226  sylow2blem2  15257  efgsp1  15371  efgrelexlemb  15384  mulgmhm  15452  mulgghm  15453  iscyggen2  15493  iscyg3  15498  rnglghm  15713  rngrghm  15714  gsumdixp  15717  dvdsrcl2  15757  crngunit  15769  subrgugrp  15889  cntzsubr  15902  lmodvsdir  15976  lmodvsass  15977  lmodvsghm  16007  lsssubg  16035  lss1d  16041  islbs2  16228  issubgrpd2  16262  lidlsubg  16288  divscrng  16313  lpigen  16329  xrsdsreval  16745  expghm  16779  mulgghm2  16788  ip0r  16870  obs2ss  16958  elcls2  17140  opnnei  17186  innei  17191  iscnp4  17329  cnpnei  17330  iscncl  17335  cnnei  17348  cnconst  17350  ordthauslem  17449  1stccnp  17527  llyrest  17550  nllyrest  17551  kgenss  17577  xkoccn  17653  kqsat  17765  kqt0lem  17770  isr0  17771  fbssfi  17871  isfild  17892  filcon  17917  trfilss  17923  fgtr  17924  ufileu  17953  ufilen  17964  fmfnfmlem4  17991  fmfnfm  17992  hausflimi  18014  cnpflf2  18034  cnpflf  18035  cnflf  18036  cnpfcf  18075  cnfcf  18076  cnextcn  18100  tmdmulg  18124  clsnsg  18141  tsmsxplem1  18184  tsmsxp  18186  trust  18261  ustuqtop0  18272  ismeti  18357  isxmet2d  18359  elbl2ps  18421  elbl2  18422  xblpnfps  18427  xblpnf  18428  xbln0  18446  blin  18453  blssexps  18458  blssex  18459  blsscls2  18536  blcls  18538  blsscls  18539  metss  18540  metrest  18556  metcn  18575  metustblOLD  18612  metustbl  18613  metutopOLD  18614  psmetutop  18615  nmf2  18642  nmdvr  18708  nmoi  18764  nmoix  18765  nmoleub  18767  nghmcn  18781  xrsxmet  18842  iccntr  18854  metdsle  18884  icoopnst  18966  iocopnst  18967  icccvx  18977  pi1xfr  19082  lmmbr  19213  lmmbr2  19214  iscfil3  19228  iscau2  19232  cfilres  19251  bcthlem1  19279  bcthlem4  19282  bcthlem5  19283  ioombl  19461  iccvolcl  19463  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  ig1pcl  20100  ig1prsp  20102  aannenlem1  20247  taylplem1  20281  dvtaylp  20288  relogeftb  20481  logdivlt  20518  cxpexp  20561  rpcxpcl  20569  isppw2  20900  vmappw  20901  lgslem4  21085  lgscllem  21089  lgsneg1  21106  lgsne0  21119  nbgraf1olem5  21457  constr3cycl  21650  grpoidinvlem3  21796  isvci  22063  nmcvcn  22193  ipval2lem2  22202  ipval2lem5  22208  sspival  22239  sspimsval  22241  isblo2  22286  nmoo0  22294  blocni  22308  isph  22325  sspph  22358  hvadd4  22540  hiassdi  22595  ocsh  22787  chj4  23039  spansncol  23072  pjjsi  23204  hoscl  23250  hodcl  23252  hoadd4  23289  homco1  23306  homulass  23307  hoadddi  23308  hoadddir  23309  unoplin  23425  adjvalval  23442  hmoplin  23447  bralnfn  23453  brafnmul  23456  lnopmi  23505  lnopcoi  23508  hmops  23525  hmopm  23526  nmophmi  23536  lnfncnbd  23562  cnlnadjlem2  23573  adjlnop  23591  adjmul  23597  adjadd  23598  branmfn  23610  kbass5  23625  kbass6  23626  leop2  23629  leopadd  23637  leopmuli  23638  pjimai  23681  atcvatlem  23890  chirredlem2  23896  mdsymlem3  23910  mdsymlem5  23912  sumdmdii  23920  sumdmdlem  23923  cdj3lem2a  23941  cdj3lem2b  23942  cdj3lem3a  23944  cdj3i  23946  xreceu  24170  toslub  24193  tosglb  24194  xrstos  24203  hasheuni  24477  ballotlemirc  24791  txpcon  24921  cvmscld  24962  2cprodeq2dv  25253  dfrdg2  25425  wsuclem  25578  nobndlem8  25656  brbtwn2  25846  ax5seglem1  25869  ax5seglem2  25870  axcontlem4  25908  segconeu  25947  linecom  26086  linethru  26089  lineintmo  26093  mblfinlem1  26245  mblfinlem3  26247  ismblfin  26249  cnambfre  26257  itg2addnclem2  26259  ftc1anclem1  26282  ftc1anclem5  26286  ftc1anclem6  26287  ftc2nc  26291  areacirclem2  26295  areacirclem4  26297  areacirclem5  26298  areacirc  26299  fnemeet2  26398  fnejoin2  26400  fzmul  26446  subspopn  26460  isbndx  26493  isbnd2  26494  isbnd3  26495  ssbnd  26499  prdstotbnd  26505  heibor1  26521  rrnmet  26540  rngonegmn1l  26567  rngohomco  26592  rngoisocnv  26599  rngoisoco  26600  crngohomfo  26618  isidlc  26627  rngoidl  26636  prnc  26679  ispridlc  26682  oddcomabszz  27009  acongtr  27045  rpnnen3lem  27104  islssfg  27147  lmhmfgsplit  27163  unxpwdom3  27235  islindf3  27275  hbtlem7  27308  sdrgacs  27488  hashgcdeq  27496  dvconstbi  27530  ioovolcl  27720  2if2  28055  otsndisj  28068  ralxfrd2  28075  elovmpt3rab1  28095  elfz0fzfz0  28125  elfzonelfzo  28143  el2fzo  28149  swrdswrd  28221  usg2wlkeq  28330  usgra2pthlem1  28336  wwlknimp  28357  3cyclfrgrarn1  28464  3cyclfrgrarn  28465  4cycl2vnunb  28469  frgrancvvdeqlemB  28489  usgreghash2spotv  28517  2spotmdisj  28519  bnj1204  29443  cvrval2  30134  glbconxN  30237  hlrelat5N  30260  cvratlem  30280  cvrat2  30288  athgt  30315  3dim2  30327  llnn0  30375  lplnn0N  30406  lvoln0N  30450  snatpsubN  30609  paddasslem18  30696  pmod1i  30707  lhpexle2  30869  lhpexle3lem  30870  lhpexle3  30871  ldilcnv  30974  trlcnv  31024  trlnidatb  31036  cdleme32snaw  31294  cdleme32fvaw  31298  cdleme42ke  31344  cdlemeg46gf  31392  cdleme50trn12  31411  cdlemg1cex  31447  cdlemb3  31465  tgrpgrplem  31608  tgrpabl  31610  tendoplcl2  31637  tendo0pl  31650  tendoicl  31655  tendoipl  31656  cdlemkid3N  31792  tendoex  31834  erngdvlem4  31850  erngdvlem4-rN  31858  dib1dim  32025  dib1dim2  32028  dihglbcpreN  32160  dihmeetALTN  32187  dih1dimatlem  32189  dihatlat  32194
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator