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  2674  moi2  2980  sbc3ie  3094  preq12bg  3828  reuhypd  4598  f1imass  5830  fcof1o  5845  weisoeq  5895  curry1f  6254  curry2f  6256  riota5OLD  6373  f1ofveu  6381  f1ocnvfv3  6382  tfrlem11  6446  oalimcl  6600  oeordsuc  6634  oelim2  6635  nneob  6692  mapxpen  7070  findcard  7142  wemaplem3  7308  en2eqpr  7682  infxpabs  7883  infxp  7886  cfflb  7930  cfsmolem  7941  isf32lem12  8035  fin1a2lem9  8079  fin1a2s  8085  axcc3  8109  axdc3lem4  8124  zornn0g  8177  pwfseqlem4  8329  tskwun  8451  tskint  8452  tskxp  8454  tskmap  8455  gruf  8478  gruwun  8480  grutsk1  8488  addcanpi  8568  ltapi  8572  mul4  9026  add4  9072  2addsub  9110  addsubeq4  9111  muladd  9257  ltleadd  9302  receu  9458  p1le  9644  lemul12b  9658  lbinfm  9752  zdiv  10129  fzind  10157  fnn0ind  10158  uzss  10295  zbtwnre  10361  qmulcl  10381  qreccl  10383  xrlttr  10521  xaddass  10616  xmulasslem3  10653  xmulass  10654  xadddilem  10661  xrsupsslem  10672  xrinfmsslem  10673  supxrunb1  10685  ixxin  10720  ioo0  10728  ico0  10749  ioc0  10750  icc0  10751  iooshf  10775  prunioo  10811  ioojoin  10813  elfz5  10837  fzind2  10970  mulexpz  11189  expsub  11196  digit2  11281  digit1  11282  facndiv  11348  faclbnd4lem4  11356  faclbnd4  11357  faclbnd5  11358  bccmpl  11369  bcval5  11377  bcpasc  11380  swrdccat1  11507  swrdccat2  11508  cats1un  11523  crim  11647  absmax  11860  ello12r  12038  elo12r  12049  climshftlem  12095  2sumeq2dv  12225  expcnv  12369  rpnnen2lem7  12546  dvdsval3  12582  dvdsnegb  12593  muldvds1  12600  muldvds2  12601  dvdscmul  12602  dvdsmulc  12603  dvdsmulcr  12605  dvds2ln  12606  divalgb  12650  ndvdssub  12653  gcddiv  12775  rpexp1i  12847  phiprmpw  12891  pythagtriplem1  12916  pockthg  13000  infpnlem1  13004  4sqlem3  13044  0ramcl  13117  firest  13386  imasaddfnlem  13479  imasleval  13492  xpsfrn2  13521  mrerintcl  13548  iscatd  13624  lubid  14165  clatleglb  14279  mreclat  14339  pslem  14364  grplmulf1o  14591  grplactcnv  14613  mulgnn0subcl  14629  mulgsubcl  14630  mulgdir  14641  issubg2  14685  cycsubgcl  14692  cycsubgss  14693  nmzsubg  14707  eqgen  14719  ghmmulg  14744  conjghm  14762  odeq  14914  odval2  14915  odf1  14924  dfod2  14926  gexdvds  14944  gexdvds2  14945  gexcl2  14949  gexdvds3  14950  sylow2blem2  14981  efgsp1  15095  efgrelexlemb  15108  mulgmhm  15176  mulgghm  15177  iscyggen2  15217  iscyg3  15222  rnglghm  15437  rngrghm  15438  gsumdixp  15441  dvdsrcl2  15481  crngunit  15493  subrgugrp  15613  cntzsubr  15626  lmodvsdir  15701  lmodvsass  15703  lmodvsghm  15735  lsssubg  15763  lss1d  15769  islbs2  15956  issubgrpd2  15990  lidlsubg  16016  divscrng  16041  lpigen  16057  xrsdsreval  16472  expghm  16506  mulgghm2  16515  ip0r  16597  obs2ss  16685  elcls2  16867  opnnei  16913  innei  16918  cnpnei  17049  iscncl  17054  cnconst  17068  ordthauslem  17167  1stccnp  17244  llyrest  17267  nllyrest  17268  kgenss  17294  xkoccn  17369  kqsat  17478  kqt0lem  17483  isr0  17484  fbssfi  17584  isfild  17605  filcon  17630  trfilss  17636  fgtr  17637  ufileu  17666  ufilen  17677  fmfnfmlem4  17704  fmfnfm  17705  hausflimi  17727  cnpflf2  17747  cnpflf  17748  cnflf  17749  cnpfcf  17788  cnfcf  17789  tmdmulg  17827  clsnsg  17844  tsmsxplem1  17887  tsmsxp  17889  ismeti  17942  isxmet2d  17944  elbl2  18002  xblpnf  18005  xbln0  18017  blin  18022  blssex  18025  blsscls2  18102  blcls  18104  blsscls  18105  metss  18106  metrest  18122  metcn  18141  nmf2  18167  nmdvr  18233  nmoi  18289  nmoix  18290  nmoleub  18292  nghmcn  18306  xrsxmet  18367  iccntr  18378  metdsle  18408  icoopnst  18490  iocopnst  18491  icccvx  18501  pi1xfr  18606  lmmbr  18737  lmmbr2  18738  iscfil3  18752  iscau2  18756  cfilres  18775  bcthlem1  18799  bcthlem4  18802  bcthlem5  18803  ioombl  18975  iccvolcl  18977  mbfi1fseqlem3  19125  mbfi1fseqlem4  19126  mbfi1fseqlem5  19127  dvmptfsum  19375  ig1pcl  19614  ig1prsp  19616  aannenlem1  19761  taylplem1  19795  dvtaylp  19802  relogeftb  19991  logdivlt  20025  cxpexp  20068  rpcxpcl  20076  isppw2  20406  vmappw  20407  lgslem4  20591  lgscllem  20595  lgsneg1  20612  lgsne0  20625  grpoidinvlem3  20926  isvci  21193  nmcvcn  21323  ipval2lem2  21332  ipval2lem5  21338  sspival  21369  sspimsval  21371  isblo2  21416  nmoo0  21424  blocni  21438  isph  21455  sspph  21488  hvadd4  21670  hiassdi  21725  ocsh  21917  chj4  22169  spansncol  22202  pjjsi  22334  hoscl  22380  hodcl  22382  hoadd4  22419  homco1  22436  homulass  22437  hoadddi  22438  hoadddir  22439  unoplin  22555  adjvalval  22572  hmoplin  22577  bralnfn  22583  brafnmul  22586  lnopmi  22635  lnopcoi  22638  hmops  22655  hmopm  22656  nmophmi  22666  lnfncnbd  22692  cnlnadjlem2  22703  adjlnop  22721  adjmul  22727  adjadd  22728  branmfn  22740  kbass5  22755  kbass6  22756  leop2  22759  leopadd  22767  leopmuli  22768  pjimai  22811  atcvatlem  23020  chirredlem2  23026  mdsymlem3  23040  mdsymlem5  23042  sumdmdii  23050  sumdmdlem  23053  cdj3lem2a  23071  cdj3lem2b  23072  cdj3lem3a  23074  cdj3i  23076  abfmpeld  23215  abfmpel  23216  xreceu  23320  trust  23441  metustbl  23508  metutop  23509  hasheuni  23651  ballotlemirc  23963  txpcon  24047  cvmscld  24088  2cprodeq2dv  24428  dfrdg2  24537  nobndlem8  24738  brbtwn2  24919  ax5seglem1  24942  ax5seglem2  24943  axcontlem4  24981  segconeu  25020  linecom  25159  linethru  25162  lineintmo  25166  itg2addnclem2  25318  areacirclem4  25344  areacirclem5  25346  areacirclem6  25347  areacirc  25348  fnemeet2  25465  fnejoin2  25467  infmrlbOLD  25571  fzmul  25592  subspopn  25615  isbndx  25654  isbnd2  25655  isbnd3  25656  ssbnd  25660  prdstotbnd  25666  heibor1  25682  rrnmet  25701  rngonegmn1l  25728  rngohomco  25753  rngoisocnv  25760  rngoisoco  25761  crngohomfo  25779  isidlc  25788  rngoidl  25797  prnc  25840  ispridlc  25843  oddcomabszz  26177  acongtr  26213  rpnnen3lem  26272  islssfg  26316  lmhmfgsplit  26332  unxpwdom3  26404  islindf3  26444  hbtlem7  26477  sdrgacs  26657  hashgcdeq  26665  dvconstbi  26699  ioovolcl  26890  fvtp1g  27237  hashunx  27294  nbgraf1olem5  27392  constr3cycl  27545  3cyclfrgrarn1  27604  3cyclfrgrarn  27605  4cycl2vnunb  27609  frgrancvvdeqlemB  27630  bnj1204  28553  cvrval2  29282  glbconxN  29385  hlrelat5N  29408  cvratlem  29428  cvrat2  29436  athgt  29463  3dim2  29475  llnn0  29523  lplnn0N  29554  lvoln0N  29598  snatpsubN  29757  paddasslem18  29844  pmod1i  29855  lhpexle2  30017  lhpexle3lem  30018  lhpexle3  30019  ldilcnv  30122  trlcnv  30172  trlnidatb  30184  cdleme32snaw  30442  cdleme32fvaw  30446  cdleme42ke  30492  cdlemeg46gf  30540  cdleme50trn12  30559  cdlemg1cex  30595  cdlemb3  30613  tgrpgrplem  30756  tgrpabl  30758  tendoplcl2  30785  tendo0pl  30798  tendoicl  30803  tendoipl  30804  cdlemkid3N  30940  tendoex  30982  erngdvlem4  30998  erngdvlem4-rN  31006  dib1dim  31173  dib1dim2  31176  dihglbcpreN  31308  dihmeetALTN  31335  dih1dimatlem  31337  dihatlat  31342
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