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

Theorem 3expa 1153
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 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anidm23  1243  mp3an2  1267  mpd3an3  1280  rgen3  2763  moi2  3075  sbc3ie  3190  preq12bg  3937  reuhypd  4709  fvtp1g  5901  f1imass  5969  fcof1o  5985  weisoeq  6035  curry1f  6399  curry2f  6401  riota5OLD  6535  f1ofveu  6543  f1ocnvfv3  6544  tfrlem11  6608  oalimcl  6762  oeordsuc  6796  oelim2  6797  nneob  6854  mapxpen  7232  findcard  7306  wemaplem3  7473  en2eqpr  7847  infxpabs  8048  infxp  8051  cfflb  8095  cfsmolem  8106  isf32lem12  8200  fin1a2lem9  8244  fin1a2s  8250  axcc3  8274  axdc3lem4  8289  zornn0g  8341  pwfseqlem4  8493  tskwun  8615  tskint  8616  tskxp  8618  tskmap  8619  gruf  8642  gruwun  8644  grutsk1  8652  addcanpi  8732  ltapi  8736  mul4  9191  add4  9237  2addsub  9275  addsubeq4  9276  muladd  9422  ltleadd  9467  receu  9623  p1le  9809  lemul12b  9823  lbinfm  9917  zdiv  10296  fzind  10324  fnn0ind  10325  uzss  10462  zbtwnre  10528  qmulcl  10548  qreccl  10550  xrlttr  10689  xaddass  10784  xmulasslem3  10821  xmulass  10822  xadddilem  10829  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  ixxin  10889  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  iooshf  10945  prunioo  10981  ioojoin  10983  elfz5  11007  fzind2  11153  mulexpz  11375  expsub  11382  digit2  11467  digit1  11468  facndiv  11534  faclbnd4lem4  11542  faclbnd4  11543  faclbnd5  11544  bccmpl  11555  bcval5  11564  bcpasc  11567  hashunx  11615  swrdccat1  11729  swrdccat2  11730  cats1un  11745  crim  11875  absmax  12088  ello12r  12266  elo12r  12277  climshftlem  12323  2sumeq2dv  12454  expcnv  12598  rpnnen2lem7  12775  dvdsval3  12811  dvdsnegb  12822  muldvds1  12829  muldvds2  12830  dvdscmul  12831  dvdsmulc  12832  dvdsmulcr  12834  dvds2ln  12835  divalgb  12879  ndvdssub  12882  gcddiv  13004  rpexp1i  13076  phiprmpw  13120  pythagtriplem1  13145  pockthg  13229  infpnlem1  13233  4sqlem3  13273  0ramcl  13346  firest  13615  imasaddfnlem  13708  imasleval  13721  xpsfrn2  13750  mrerintcl  13777  iscatd  13853  lubid  14394  clatleglb  14508  mreclat  14568  pslem  14593  grplmulf1o  14820  grplactcnv  14842  mulgnn0subcl  14858  mulgsubcl  14859  mulgdir  14870  issubg2  14914  cycsubgcl  14921  cycsubgss  14922  nmzsubg  14936  eqgen  14948  ghmmulg  14973  conjghm  14991  odeq  15143  odval2  15144  odf1  15153  dfod2  15155  gexdvds  15173  gexdvds2  15174  gexcl2  15178  gexdvds3  15179  sylow2blem2  15210  efgsp1  15324  efgrelexlemb  15337  mulgmhm  15405  mulgghm  15406  iscyggen2  15446  iscyg3  15451  rnglghm  15666  rngrghm  15667  gsumdixp  15670  dvdsrcl2  15710  crngunit  15722  subrgugrp  15842  cntzsubr  15855  lmodvsdir  15929  lmodvsass  15930  lmodvsghm  15960  lsssubg  15988  lss1d  15994  islbs2  16181  issubgrpd2  16215  lidlsubg  16241  divscrng  16266  lpigen  16282  xrsdsreval  16698  expghm  16732  mulgghm2  16741  ip0r  16823  obs2ss  16911  elcls2  17093  opnnei  17139  innei  17144  iscnp4  17281  cnpnei  17282  iscncl  17287  cnnei  17300  cnconst  17302  ordthauslem  17401  1stccnp  17478  llyrest  17501  nllyrest  17502  kgenss  17528  xkoccn  17604  kqsat  17716  kqt0lem  17721  isr0  17722  fbssfi  17822  isfild  17843  filcon  17868  trfilss  17874  fgtr  17875  ufileu  17904  ufilen  17915  fmfnfmlem4  17942  fmfnfm  17943  hausflimi  17965  cnpflf2  17985  cnpflf  17986  cnflf  17987  cnpfcf  18026  cnfcf  18027  cnextcn  18051  tmdmulg  18075  clsnsg  18092  tsmsxplem1  18135  tsmsxp  18137  trust  18212  ustuqtop0  18223  ismeti  18308  isxmet2d  18310  elbl2ps  18372  elbl2  18373  xblpnfps  18378  xblpnf  18379  xbln0  18397  blin  18404  blssexps  18409  blssex  18410  blsscls2  18487  blcls  18489  blsscls  18490  metss  18491  metrest  18507  metcn  18526  metustblOLD  18563  metustbl  18564  metutopOLD  18565  psmetutop  18566  nmf2  18593  nmdvr  18659  nmoi  18715  nmoix  18716  nmoleub  18718  nghmcn  18732  xrsxmet  18793  iccntr  18805  metdsle  18835  icoopnst  18917  iocopnst  18918  icccvx  18928  pi1xfr  19033  lmmbr  19164  lmmbr2  19165  iscfil3  19179  iscau2  19183  cfilres  19202  bcthlem1  19230  bcthlem4  19233  bcthlem5  19234  ioombl  19412  iccvolcl  19414  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  ig1pcl  20051  ig1prsp  20053  aannenlem1  20198  taylplem1  20232  dvtaylp  20239  relogeftb  20432  logdivlt  20469  cxpexp  20512  rpcxpcl  20520  isppw2  20851  vmappw  20852  lgslem4  21036  lgscllem  21040  lgsneg1  21057  lgsne0  21070  nbgraf1olem5  21408  constr3cycl  21601  grpoidinvlem3  21747  isvci  22014  nmcvcn  22144  ipval2lem2  22153  ipval2lem5  22159  sspival  22190  sspimsval  22192  isblo2  22237  nmoo0  22245  blocni  22259  isph  22276  sspph  22309  hvadd4  22491  hiassdi  22546  ocsh  22738  chj4  22990  spansncol  23023  pjjsi  23155  hoscl  23201  hodcl  23203  hoadd4  23240  homco1  23257  homulass  23258  hoadddi  23259  hoadddir  23260  unoplin  23376  adjvalval  23393  hmoplin  23398  bralnfn  23404  brafnmul  23407  lnopmi  23456  lnopcoi  23459  hmops  23476  hmopm  23477  nmophmi  23487  lnfncnbd  23513  cnlnadjlem2  23524  adjlnop  23542  adjmul  23548  adjadd  23549  branmfn  23561  kbass5  23576  kbass6  23577  leop2  23580  leopadd  23588  leopmuli  23589  pjimai  23632  atcvatlem  23841  chirredlem2  23847  mdsymlem3  23861  mdsymlem5  23863  sumdmdii  23871  sumdmdlem  23874  cdj3lem2a  23892  cdj3lem2b  23893  cdj3lem3a  23895  cdj3i  23897  xreceu  24121  toslub  24144  tosglb  24145  xrstos  24154  hasheuni  24428  ballotlemirc  24742  txpcon  24872  cvmscld  24913  2cprodeq2dv  25204  dfrdg2  25366  nobndlem8  25567  brbtwn2  25748  ax5seglem1  25771  ax5seglem2  25772  axcontlem4  25810  segconeu  25849  linecom  25988  linethru  25991  lineintmo  25995  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  cnambfre  26154  itg2addnclem2  26156  areacirclem4  26183  areacirclem5  26185  areacirclem6  26186  areacirc  26187  fnemeet2  26286  fnejoin2  26288  fzmul  26334  subspopn  26348  isbndx  26381  isbnd2  26382  isbnd3  26383  ssbnd  26387  prdstotbnd  26393  heibor1  26409  rrnmet  26428  rngonegmn1l  26455  rngohomco  26480  rngoisocnv  26487  rngoisoco  26488  crngohomfo  26506  isidlc  26515  rngoidl  26524  prnc  26567  ispridlc  26570  oddcomabszz  26897  acongtr  26933  rpnnen3lem  26992  islssfg  27036  lmhmfgsplit  27052  unxpwdom3  27124  islindf3  27164  hbtlem7  27197  sdrgacs  27377  hashgcdeq  27385  dvconstbi  27419  ioovolcl  27609  2if2  27941  otsndisj  27953  elfzonelfzo  27992  swrdswrd  28011  usgra2pthlem1  28040  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  4cycl2vnunb  28121  frgrancvvdeqlemB  28141  usgreghash2spotv  28169  2spotmdisj  28171  bnj1204  29087  cvrval2  29757  glbconxN  29860  hlrelat5N  29883  cvratlem  29903  cvrat2  29911  athgt  29938  3dim2  29950  llnn0  29998  lplnn0N  30029  lvoln0N  30073  snatpsubN  30232  paddasslem18  30319  pmod1i  30330  lhpexle2  30492  lhpexle3lem  30493  lhpexle3  30494  ldilcnv  30597  trlcnv  30647  trlnidatb  30659  cdleme32snaw  30917  cdleme32fvaw  30921  cdleme42ke  30967  cdlemeg46gf  31015  cdleme50trn12  31034  cdlemg1cex  31070  cdlemb3  31088  tgrpgrplem  31231  tgrpabl  31233  tendoplcl2  31260  tendo0pl  31273  tendoicl  31278  tendoipl  31279  cdlemkid3N  31415  tendoex  31457  erngdvlem4  31473  erngdvlem4-rN  31481  dib1dim  31648  dib1dim2  31651  dihglbcpreN  31783  dihmeetALTN  31810  dih1dimatlem  31812  dihatlat  31817
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator