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

Theorem 3expa 1197
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 1196 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 371  df-3an 976
This theorem is referenced by:  3anidm23  1288  mp3an2  1313  mpd3an3  1326  rgen3  2869  moi2  3266  sbc3ie  3391  2if2  3974  preq12bg  4194  prel12g  4195  reuhypd  4664  otsndisj  4742  fvtp1g  6106  f1imass  6157  weisoeq  6236  f1ofveu  6276  f1ocnvfv3  6277  curry1f  6879  curry2f  6881  funsssuppss  6928  tfrlem11  7059  oalimcl  7211  oeordsuc  7245  oelim2  7246  nneob  7303  mapxpen  7685  findcard  7761  wemaplem3  7976  en2eqpr  8388  infxpabs  8595  infxp  8598  cfflb  8642  cfsmolem  8653  isf32lem12  8747  fin1a2lem9  8791  fin1a2s  8797  axcc3  8821  axdc3lem4  8836  zornn0g  8888  pwfseqlem4  9043  tskwun  9165  tskint  9166  tskxp  9168  tskmap  9169  gruf  9192  gruwun  9194  grutsk1  9202  addcanpi  9280  ltapi  9284  mul4  9752  add4  9799  2addsub  9839  addsubeq4  9840  muladd  9996  ltleadd  10042  receu  10201  p1le  10392  lemul12b  10406  lbinfm  10503  zdiv  10940  fzind  10969  fnn0ind  10970  uzss  11112  zbtwnre  11191  qmulcl  11211  qreccl  11213  xrlttr  11357  xaddass  11452  xmulasslem3  11489  xmulass  11490  xadddilem  11497  xrsupsslem  11509  xrinfmsslem  11510  supxrunb1  11522  ixxin  11557  ioo0  11565  ico0  11586  ioc0  11587  icc0  11588  iooshf  11614  prunioo  11660  ioojoin  11662  elfz5  11691  elfz0fzfz0  11790  elfzonelfzo  11894  fzind2  11906  mulexpz  12188  expsub  12195  digit2  12281  digit1  12282  facndiv  12348  faclbnd4lem4  12356  faclbnd4  12357  faclbnd5  12358  bccmpl  12369  bcval5  12378  bcpasc  12381  hashunx  12436  ccatrn  12588  swrdspsleq  12655  swrdccat1  12664  swrdccat2  12665  swrdswrd  12667  cats1un  12683  crim  12930  absmax  13144  ello12r  13322  elo12r  13333  climshftlem  13379  2sumeq2dv  13509  expcnv  13657  2cprodeq2dv  13714  rpnnen2lem7  13936  dvdsval3  13972  dvdsnegb  13983  muldvds1  13990  muldvds2  13991  dvdscmul  13992  dvdsmulc  13993  dvdsmulcr  13995  dvds2ln  13996  divalgb  14044  ndvdssub  14047  gcddiv  14169  rpexp1i  14244  phiprmpw  14288  pythagtriplem1  14322  pockthg  14406  infpnlem1  14410  4sqlem3  14450  0ramcl  14523  firest  14812  imasaddfnlem  14907  imasleval  14920  xpsfrn2  14949  mrerintcl  14976  iscatd  15052  clatleglb  15735  mreclatBAD  15796  pslem  15815  mrcmndind  15976  grplmulf1o  16091  grplactcnv  16117  mulgnn0subcl  16134  mulgsubcl  16135  mulgdir  16146  issubg2  16195  issubgrpd2  16196  cycsubgcl  16206  cycsubgss  16207  nmzsubg  16221  eqgen  16233  ghmmulg  16258  conjghm  16276  symgfixfo  16443  odeq  16553  odval2  16554  odf1  16563  dfod2  16565  gexdvds  16583  gexdvds2  16584  gexcl2  16588  gexdvds3  16589  sylow2blem2  16620  efgsp1  16734  efgrelexlemb  16747  mulgmhm  16815  mulgghm  16816  iscyggen2  16863  iscyg3  16868  srglmhm  17165  srgrmhm  17166  ringlghm  17229  ringrghm  17230  gsumdixpOLD  17236  gsumdixp  17237  dvdsrcl2  17278  crngunit  17290  kerf1hrm  17371  subrgugrp  17427  cntzsubr  17440  lmodvsdir  17515  lmodvsass  17516  lmodvsghm  17550  lsssubg  17582  lss1d  17588  islbs2  17779  lidlsubg  17841  lidlsubcl  17842  quscrng  17867  lpigen  17883  xrsdsreval  18442  expghm  18507  expghmOLD  18508  mulgghm2  18509  mulgghm2OLD  18512  ip0r  18650  obs2ss  18738  islindf3  18839  scmatscm  18993  scmataddcl  18996  scmatsubcl  18997  scmatfo  19010  matunit  19158  cpmatelimp  19191  cpmatelimp2  19193  cpmatinvcl  19196  cpmatmcl  19198  mat2pmatf  19207  m2cpmf  19221  cpm2mf  19231  m2cpmfo  19235  m2cpminv  19239  decpmataa0  19247  pm2mpf  19277  pm2mpf1  19278  idpm2idmp  19280  pm2mpfo  19293  elcls2  19553  opnnei  19599  innei  19604  iscnp4  19742  cnpnei  19743  iscncl  19748  cnnei  19761  cnconst  19763  ordthauslem  19862  bwth  19888  1stccnp  19941  llyrest  19964  nllyrest  19965  kgenss  20022  xkoccn  20098  kqsat  20210  kqt0lem  20215  isr0  20216  fbssfi  20316  isfild  20337  filcon  20362  trfilss  20368  fgtr  20369  ufileu  20398  ufilen  20409  fmfnfmlem4  20436  fmfnfm  20437  hausflimi  20459  cnpflf2  20479  cnpflf  20480  cnflf  20481  cnpfcf  20520  cnfcf  20521  cnextcn  20545  tmdmulg  20569  clsnsg  20586  tsmsxplem1  20633  tsmsxp  20635  trust  20710  ustuqtop0  20721  ismeti  20806  isxmet2d  20808  elbl2ps  20870  elbl2  20871  xblpnfps  20876  xblpnf  20877  xbln0  20895  blin  20902  blssexps  20907  blssex  20908  blsscls2  20985  blcls  20987  blsscls  20988  metss  20989  metrest  21005  metcn  21024  metustblOLD  21061  metustbl  21062  metutopOLD  21063  psmetutop  21064  nmf2  21091  nmdvr  21157  nmoi  21213  nmoix  21214  nmoleub  21216  nghmcn  21230  xrsxmet  21292  iccntr  21304  metdsle  21334  icoopnst  21417  iocopnst  21418  icccvx  21428  pi1xfr  21533  lmmbr  21675  lmmbr2  21676  iscfil3  21690  iscau2  21694  cfilres  21713  bcthlem1  21741  bcthlem4  21744  bcthlem5  21745  rrxmet  21813  ioombl  21953  iccvolcl  21955  ioovolcl  21957  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  ig1pcl  22554  ig1prsp  22556  aannenlem1  22702  taylplem1  22736  dvtaylp  22743  relogeftb  22947  logdivlt  22984  cxpexp  23027  rpcxpcl  23035  isppw2  23367  vmappw  23368  lgslem4  23552  lgscllem  23556  lgsneg1  23573  lgsne0  23586  brbtwn2  24186  ax5seglem1  24209  ax5seglem2  24210  axcontlem4  24248  nbgraf1olem5  24423  constr3cycl  24639  wwlknimp  24665  usg2wlkeq  24686  wwlknred  24701  wwlknext  24702  clwwlknprop  24750  3cyclfrgrarn1  24990  3cyclfrgrarn  24991  4cycl2vnunb  24995  frgrancvvdeqlemB  25016  usgreghash2spotv  25044  2spotmdisj  25046  grpoidinvlem3  25186  isvci  25453  nmcvcn  25583  ipval2lem2  25592  ipval2lem5  25598  sspival  25629  sspimsval  25631  isblo2  25676  nmoo0  25684  blocni  25698  isph  25715  sspph  25748  hvadd4  25931  hiassdi  25986  ocsh  26179  chj4  26431  spansncol  26464  pjjsi  26596  hoscl  26642  hodcl  26644  hoadd4  26681  homco1  26698  homulass  26699  hoadddi  26700  hoadddir  26701  unoplin  26817  adjvalval  26834  hmoplin  26839  bralnfn  26845  brafnmul  26848  lnopmi  26897  lnopcoi  26900  hmops  26917  hmopm  26918  nmophmi  26928  lnfncnbd  26954  cnlnadjlem2  26965  adjlnop  26983  adjmul  26989  adjadd  26990  branmfn  27002  kbass5  27017  kbass6  27018  leop2  27021  leopadd  27029  leopmuli  27030  pjimai  27073  atcvatlem  27282  chirredlem2  27288  mdsymlem3  27302  mdsymlem5  27304  sumdmdii  27312  sumdmdlem  27315  cdj3lem2a  27333  cdj3lem2b  27334  cdj3lem3a  27336  cdj3i  27338  xreceu  27596  toslublem  27633  tosglblem  27635  ogrpaddltbi  27687  archiabllem1b  27714  archiabllem2c  27717  archiabl  27720  slmdvsdir  27737  slmdvsass  27738  pstmxmet  27854  ordtconlem1  27884  hasheuni  28069  ballotlemirc  28448  signswmnd  28492  txpcon  28655  cvmscld  28696  elmpps  28911  dfrdg2  29204  wsuclem  29357  nobndlem8  29435  segconeu  29637  linecom  29776  linethru  29779  lineintmo  29783  heicant  30025  mblfinlem1  30027  mblfinlem3  30029  ismblfin  30031  cnambfre  30039  itg2addnclem2  30043  ftc1anclem1  30066  ftc1anclem5  30070  ftc1anclem6  30071  ftc2nc  30075  areacirclem2  30084  areacirclem4  30086  areacirclem5  30087  areacirc  30088  fnemeet2  30161  fnejoin2  30163  fzmul  30209  subspopn  30221  isbndx  30254  isbnd2  30255  isbnd3  30256  ssbnd  30260  prdstotbnd  30266  heibor1  30282  rrnmet  30301  rngonegmn1l  30328  rngohomco  30353  rngoisocnv  30360  rngoisoco  30361  crngohomfo  30379  isidlc  30388  rngoidl  30397  prnc  30440  ispridlc  30443  oddcomabszz  30856  acongtr  30892  rpnnen3lem  30949  islssfg  30992  lmhmfgsplit  31008  unxpwdom3  31017  hbtlem7  31050  sdrgacs  31126  hashgcdeq  31134  iocmbl  31156  nzss  31198  dvconstbi  31215  iccdifprioo  31510  dvnmul  31694  fourierdlem74  31917  fourierdlem75  31918  ralxfrd2  32257  el2fzo  32293  usgra2pthlem1  32307  fullestrcsetc  32623  fullsetcestrc  32638  rnghmsubcsetclem2  32659  rhmsubcsetclem2  32702  rhmsubcrngclem2  32708  lcoss  32907  snlindsntorlem  32941  bnj1204  33936  cvrval2  34874  glbconxN  34977  hlrelat5N  35000  cvratlem  35020  cvrat2  35028  athgt  35055  3dim2  35067  llnn0  35115  lplnn0N  35146  lvoln0N  35190  snatpsubN  35349  paddasslem18  35436  pmod1i  35447  lhpexle2  35609  lhpexle3lem  35610  lhpexle3  35611  ldilcnv  35714  trlcnv  35765  trlnidatb  35777  cdleme32snaw  36036  cdleme32fvaw  36040  cdleme42ke  36086  cdlemeg46gf  36134  cdleme50trn12  36153  cdlemg1cex  36189  cdlemb3  36207  tgrpgrplem  36350  tgrpabl  36352  tendoplcl2  36379  tendo0pl  36392  tendoicl  36397  tendoipl  36398  cdlemkid3N  36534  tendoex  36576  erngdvlem4  36592  erngdvlem4-rN  36600  dib1dim  36767  dib1dim2  36770  dihglbcpreN  36902  dihmeetALTN  36929  dih1dimatlem  36931  dihatlat  36936
  Copyright terms: Public domain W3C validator