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

Theorem 3expa 1180
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 1179 . 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 958
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 960
This theorem is referenced by:  3anidm23  1270  mp3an2  1295  mpd3an3  1308  rgen3  2803  moi2  3129  sbc3ie  3252  2if2  3825  preq12bg  4039  prel12g  4040  reuhypd  4507  fvtp1g  5915  f1imass  5964  fcof1o  5984  weisoeq  6033  f1ofveu  6074  f1ocnvfv3  6075  curry1f  6655  curry2f  6657  funsssuppss  6704  tfrlem11  6833  oalimcl  6987  oeordsuc  7021  oelim2  7022  nneob  7079  mapxpen  7465  findcard  7539  wemaplem3  7750  en2eqpr  8162  infxpabs  8369  infxp  8372  cfflb  8416  cfsmolem  8427  isf32lem12  8521  fin1a2lem9  8565  fin1a2s  8571  axcc3  8595  axdc3lem4  8610  zornn0g  8662  pwfseqlem4  8817  tskwun  8939  tskint  8940  tskxp  8942  tskmap  8943  gruf  8966  gruwun  8968  grutsk1  8976  addcanpi  9056  ltapi  9060  mul4  9526  add4  9573  2addsub  9612  addsubeq4  9613  muladd  9765  ltleadd  9810  receu  9969  p1le  10160  lemul12b  10174  lbinfm  10271  zdiv  10700  fzind  10728  fnn0ind  10729  uzss  10869  zbtwnre  10939  qmulcl  10959  qreccl  10961  xrlttr  11105  xaddass  11200  xmulasslem3  11237  xmulass  11238  xadddilem  11245  xrsupsslem  11257  xrinfmsslem  11258  supxrunb1  11270  ixxin  11305  ioo0  11313  ico0  11334  ioc0  11335  icc0  11336  iooshf  11362  prunioo  11401  ioojoin  11403  elfz5  11432  elfz0fzfz0  11472  elfzonelfzo  11611  fzind2  11621  mulexpz  11888  expsub  11895  digit2  11981  digit1  11982  facndiv  12048  faclbnd4lem4  12056  faclbnd4  12057  faclbnd5  12058  bccmpl  12069  bcval5  12078  bcpasc  12081  hashunx  12133  swrdspsleq  12326  swrdccat1  12335  swrdccat2  12336  swrdswrd  12338  cats1un  12354  crim  12588  absmax  12801  ello12r  12979  elo12r  12990  climshftlem  13036  2sumeq2dv  13166  expcnv  13309  rpnnen2lem7  13486  dvdsval3  13522  dvdsnegb  13533  muldvds1  13540  muldvds2  13541  dvdscmul  13542  dvdsmulc  13543  dvdsmulcr  13545  dvds2ln  13546  divalgb  13591  ndvdssub  13594  gcddiv  13716  rpexp1i  13790  phiprmpw  13834  pythagtriplem1  13866  pockthg  13950  infpnlem1  13954  4sqlem3  13994  0ramcl  14067  firest  14354  imasaddfnlem  14449  imasleval  14462  xpsfrn2  14491  mrerintcl  14518  iscatd  14594  clatleglb  15279  mreclatBAD  15340  pslem  15359  mrcmndind  15476  grplmulf1o  15580  grplactcnv  15604  mulgnn0subcl  15620  mulgsubcl  15621  mulgdir  15632  issubg2  15676  issubgrpd2  15677  cycsubgcl  15687  cycsubgss  15688  nmzsubg  15702  eqgen  15714  ghmmulg  15739  conjghm  15757  symgfixfo  15925  odeq  16033  odval2  16034  odf1  16043  dfod2  16045  gexdvds  16063  gexdvds2  16064  gexcl2  16068  gexdvds3  16069  sylow2blem2  16100  efgsp1  16214  efgrelexlemb  16227  mulgmhm  16295  mulgghm  16296  iscyggen2  16338  iscyg3  16343  rnglghm  16628  rngrghm  16629  gsumdixpOLD  16635  gsumdixp  16636  dvdsrcl2  16676  crngunit  16688  subrgugrp  16808  cntzsubr  16821  lmodvsdir  16896  lmodvsass  16897  lmodvsghm  16930  lsssubg  16960  lss1d  16966  islbs2  17157  lidlsubg  17219  divscrng  17244  lpigen  17260  xrsdsreval  17702  expghm  17765  expghmOLD  17766  mulgghm2  17767  mulgghm2OLD  17770  ip0r  17908  obs2ss  17996  islindf3  18097  matunit  18326  elcls2  18520  opnnei  18566  innei  18571  iscnp4  18709  cnpnei  18710  iscncl  18715  cnnei  18728  cnconst  18730  ordthauslem  18829  bwth  18855  1stccnp  18908  llyrest  18931  nllyrest  18932  kgenss  18958  xkoccn  19034  kqsat  19146  kqt0lem  19151  isr0  19152  fbssfi  19252  isfild  19273  filcon  19298  trfilss  19304  fgtr  19305  ufileu  19334  ufilen  19345  fmfnfmlem4  19372  fmfnfm  19373  hausflimi  19395  cnpflf2  19415  cnpflf  19416  cnflf  19417  cnpfcf  19456  cnfcf  19457  cnextcn  19481  tmdmulg  19505  clsnsg  19522  tsmsxplem1  19569  tsmsxp  19571  trust  19646  ustuqtop0  19657  ismeti  19742  isxmet2d  19744  elbl2ps  19806  elbl2  19807  xblpnfps  19812  xblpnf  19813  xbln0  19831  blin  19838  blssexps  19843  blssex  19844  blsscls2  19921  blcls  19923  blsscls  19924  metss  19925  metrest  19941  metcn  19960  metustblOLD  19997  metustbl  19998  metutopOLD  19999  psmetutop  20000  nmf2  20027  nmdvr  20093  nmoi  20149  nmoix  20150  nmoleub  20152  nghmcn  20166  xrsxmet  20228  iccntr  20240  metdsle  20270  icoopnst  20353  iocopnst  20354  icccvx  20364  pi1xfr  20469  lmmbr  20611  lmmbr2  20612  iscfil3  20626  iscau2  20630  cfilres  20649  bcthlem1  20677  bcthlem4  20680  bcthlem5  20681  rrxmet  20749  ioombl  20888  iccvolcl  20890  ioovolcl  20892  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  ig1pcl  21532  ig1prsp  21534  aannenlem1  21679  taylplem1  21713  dvtaylp  21720  relogeftb  21918  logdivlt  21955  cxpexp  21998  rpcxpcl  22006  isppw2  22338  vmappw  22339  lgslem4  22523  lgscllem  22527  lgsneg1  22544  lgsne0  22557  brbtwn2  22974  ax5seglem1  22997  ax5seglem2  22998  axcontlem4  23036  nbgraf1olem5  23177  constr3cycl  23370  grpoidinvlem3  23516  isvci  23783  nmcvcn  23913  ipval2lem2  23922  ipval2lem5  23928  sspival  23959  sspimsval  23961  isblo2  24006  nmoo0  24014  blocni  24028  isph  24045  sspph  24078  hvadd4  24261  hiassdi  24316  ocsh  24509  chj4  24761  spansncol  24794  pjjsi  24926  hoscl  24972  hodcl  24974  hoadd4  25011  homco1  25028  homulass  25029  hoadddi  25030  hoadddir  25031  unoplin  25147  adjvalval  25164  hmoplin  25169  bralnfn  25175  brafnmul  25178  lnopmi  25227  lnopcoi  25230  hmops  25247  hmopm  25248  nmophmi  25258  lnfncnbd  25284  cnlnadjlem2  25295  adjlnop  25313  adjmul  25319  adjadd  25320  branmfn  25332  kbass5  25347  kbass6  25348  leop2  25351  leopadd  25359  leopmuli  25360  pjimai  25403  atcvatlem  25612  chirredlem2  25618  mdsymlem3  25632  mdsymlem5  25634  sumdmdii  25642  sumdmdlem  25645  cdj3lem2a  25663  cdj3lem2b  25664  cdj3lem3a  25666  cdj3i  25668  xreceu  25920  toslublem  25951  tosglblem  25953  xrstos  25963  ogrpaddltbi  26006  archiabllem1a  26032  archiabllem1b  26033  archiabllem2c  26036  archiabl  26039  slmdvsdir  26081  slmdvsass  26082  ordtconlem1  26208  hasheuni  26388  ballotlemirc  26762  signspval  26801  txpcon  26969  cvmscld  27010  2cprodeq2dv  27285  dfrdg2  27456  wsuclem  27609  nobndlem8  27687  segconeu  27889  linecom  28028  linethru  28031  lineintmo  28035  heicant  28270  mblfinlem1  28272  mblfinlem3  28274  ismblfin  28276  cnambfre  28284  itg2addnclem2  28288  ftc1anclem1  28311  ftc1anclem5  28315  ftc1anclem6  28316  ftc2nc  28320  areacirclem2  28329  areacirclem4  28331  areacirclem5  28332  areacirc  28333  fnemeet2  28432  fnejoin2  28434  fzmul  28480  subspopn  28492  isbndx  28525  isbnd2  28526  isbnd3  28527  ssbnd  28531  prdstotbnd  28537  heibor1  28553  rrnmet  28572  rngonegmn1l  28599  rngohomco  28624  rngoisocnv  28631  rngoisoco  28632  crngohomfo  28650  isidlc  28659  rngoidl  28668  prnc  28711  ispridlc  28714  oddcomabszz  29130  acongtr  29166  rpnnen3lem  29225  islssfg  29268  lmhmfgsplit  29284  unxpwdom3  29293  hbtlem7  29326  sdrgacs  29403  hashgcdeq  29411  iocmbl  29433  dvconstbi  29453  otsndisj  29977  ralxfrd2  29983  el2fzo  30058  usg2wlkeq  30135  usgra2pthlem1  30146  wwlknimp  30167  wwlknred  30201  wwlknext  30202  clwwlknprop  30281  3cyclfrgrarn1  30450  3cyclfrgrarn  30451  4cycl2vnunb  30455  frgrancvvdeqlemB  30477  usgreghash2spotv  30505  2spotmdisj  30507  lcoss  30679  snlindsntorlem  30713  bnj1204  31705  cvrval2  32492  glbconxN  32595  hlrelat5N  32618  cvratlem  32638  cvrat2  32646  athgt  32673  3dim2  32685  llnn0  32733  lplnn0N  32764  lvoln0N  32808  snatpsubN  32967  paddasslem18  33054  pmod1i  33065  lhpexle2  33227  lhpexle3lem  33228  lhpexle3  33229  ldilcnv  33332  trlcnv  33382  trlnidatb  33394  cdleme32snaw  33652  cdleme32fvaw  33656  cdleme42ke  33702  cdlemeg46gf  33750  cdleme50trn12  33769  cdlemg1cex  33805  cdlemb3  33823  tgrpgrplem  33966  tgrpabl  33968  tendoplcl2  33995  tendo0pl  34008  tendoicl  34013  tendoipl  34014  cdlemkid3N  34150  tendoex  34192  erngdvlem4  34208  erngdvlem4-rN  34216  dib1dim  34383  dib1dim2  34386  dihglbcpreN  34518  dihmeetALTN  34545  dih1dimatlem  34547  dihatlat  34552
  Copyright terms: Public domain W3C validator