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  2809  moi2  3121  sbc3ie  3243  preq12bg  4001  reuhypd  4779  fvtp1g  5971  f1imass  6039  fcof1o  6055  weisoeq  6105  curry1f  6469  curry2f  6471  riota5OLD  6605  f1ofveu  6613  f1ocnvfv3  6614  tfrlem11  6678  oalimcl  6832  oeordsuc  6866  oelim2  6867  nneob  6924  mapxpen  7302  findcard  7376  wemaplem3  7546  en2eqpr  7922  infxpabs  8123  infxp  8126  cfflb  8170  cfsmolem  8181  isf32lem12  8275  fin1a2lem9  8319  fin1a2s  8325  axcc3  8349  axdc3lem4  8364  zornn0g  8416  pwfseqlem4  8568  tskwun  8690  tskint  8691  tskxp  8693  tskmap  8694  gruf  8717  gruwun  8719  grutsk1  8727  addcanpi  8807  ltapi  8811  mul4  9266  add4  9312  2addsub  9350  addsubeq4  9351  muladd  9497  ltleadd  9542  receu  9698  p1le  9884  lemul12b  9898  lbinfm  9992  zdiv  10371  fzind  10399  fnn0ind  10400  uzss  10537  zbtwnre  10603  qmulcl  10623  qreccl  10625  xrlttr  10764  xaddass  10859  xmulasslem3  10896  xmulass  10897  xadddilem  10904  xrsupsslem  10916  xrinfmsslem  10917  supxrunb1  10929  ixxin  10964  ioo0  10972  ico0  10993  ioc0  10994  icc0  10995  iooshf  11020  prunioo  11056  ioojoin  11058  elfz5  11082  fzind2  11229  mulexpz  11451  expsub  11458  digit2  11543  digit1  11544  facndiv  11610  faclbnd4lem4  11618  faclbnd4  11619  faclbnd5  11620  bccmpl  11631  bcval5  11640  bcpasc  11643  hashunx  11691  swrdccat1  11805  swrdccat2  11806  cats1un  11821  crim  11951  absmax  12164  ello12r  12342  elo12r  12353  climshftlem  12399  2sumeq2dv  12530  expcnv  12674  rpnnen2lem7  12851  dvdsval3  12887  dvdsnegb  12898  muldvds1  12905  muldvds2  12906  dvdscmul  12907  dvdsmulc  12908  dvdsmulcr  12910  dvds2ln  12911  divalgb  12955  ndvdssub  12958  gcddiv  13080  rpexp1i  13152  phiprmpw  13196  pythagtriplem1  13221  pockthg  13305  infpnlem1  13309  4sqlem3  13349  0ramcl  13422  firest  13691  imasaddfnlem  13784  imasleval  13797  xpsfrn2  13826  mrerintcl  13853  iscatd  13929  lubid  14470  clatleglb  14584  mreclat  14644  pslem  14669  grplmulf1o  14896  grplactcnv  14918  mulgnn0subcl  14934  mulgsubcl  14935  mulgdir  14946  issubg2  14990  cycsubgcl  14997  cycsubgss  14998  nmzsubg  15012  eqgen  15024  ghmmulg  15049  conjghm  15067  odeq  15219  odval2  15220  odf1  15229  dfod2  15231  gexdvds  15249  gexdvds2  15250  gexcl2  15254  gexdvds3  15255  sylow2blem2  15286  efgsp1  15400  efgrelexlemb  15413  mulgmhm  15481  mulgghm  15482  iscyggen2  15522  iscyg3  15527  rnglghm  15742  rngrghm  15743  gsumdixp  15746  dvdsrcl2  15786  crngunit  15798  subrgugrp  15918  cntzsubr  15931  lmodvsdir  16005  lmodvsass  16006  lmodvsghm  16036  lsssubg  16064  lss1d  16070  islbs2  16257  issubgrpd2  16291  lidlsubg  16317  divscrng  16342  lpigen  16358  xrsdsreval  16774  expghm  16808  mulgghm2  16817  ip0r  16899  obs2ss  16987  elcls2  17169  opnnei  17215  innei  17220  iscnp4  17358  cnpnei  17359  iscncl  17364  cnnei  17377  cnconst  17379  ordthauslem  17478  1stccnp  17556  llyrest  17579  nllyrest  17580  kgenss  17606  xkoccn  17682  kqsat  17794  kqt0lem  17799  isr0  17800  fbssfi  17900  isfild  17921  filcon  17946  trfilss  17952  fgtr  17953  ufileu  17982  ufilen  17993  fmfnfmlem4  18020  fmfnfm  18021  hausflimi  18043  cnpflf2  18063  cnpflf  18064  cnflf  18065  cnpfcf  18104  cnfcf  18105  cnextcn  18129  tmdmulg  18153  clsnsg  18170  tsmsxplem1  18213  tsmsxp  18215  trust  18290  ustuqtop0  18301  ismeti  18386  isxmet2d  18388  elbl2ps  18450  elbl2  18451  xblpnfps  18456  xblpnf  18457  xbln0  18475  blin  18482  blssexps  18487  blssex  18488  blsscls2  18565  blcls  18567  blsscls  18568  metss  18569  metrest  18585  metcn  18604  metustblOLD  18641  metustbl  18642  metutopOLD  18643  psmetutop  18644  nmf2  18671  nmdvr  18737  nmoi  18793  nmoix  18794  nmoleub  18796  nghmcn  18810  xrsxmet  18871  iccntr  18883  metdsle  18913  icoopnst  18995  iocopnst  18996  icccvx  19006  pi1xfr  19111  lmmbr  19242  lmmbr2  19243  iscfil3  19257  iscau2  19261  cfilres  19280  bcthlem1  19308  bcthlem4  19311  bcthlem5  19312  ioombl  19490  iccvolcl  19492  mbfi1fseqlem3  19638  mbfi1fseqlem4  19639  mbfi1fseqlem5  19640  ig1pcl  20129  ig1prsp  20131  aannenlem1  20276  taylplem1  20310  dvtaylp  20317  relogeftb  20510  logdivlt  20547  cxpexp  20590  rpcxpcl  20598  isppw2  20929  vmappw  20930  lgslem4  21114  lgscllem  21118  lgsneg1  21135  lgsne0  21148  nbgraf1olem5  21486  constr3cycl  21679  grpoidinvlem3  21825  isvci  22092  nmcvcn  22222  ipval2lem2  22231  ipval2lem5  22237  sspival  22268  sspimsval  22270  isblo2  22315  nmoo0  22323  blocni  22337  isph  22354  sspph  22387  hvadd4  22569  hiassdi  22624  ocsh  22816  chj4  23068  spansncol  23101  pjjsi  23233  hoscl  23279  hodcl  23281  hoadd4  23318  homco1  23335  homulass  23336  hoadddi  23337  hoadddir  23338  unoplin  23454  adjvalval  23471  hmoplin  23476  bralnfn  23482  brafnmul  23485  lnopmi  23534  lnopcoi  23537  hmops  23554  hmopm  23555  nmophmi  23565  lnfncnbd  23591  cnlnadjlem2  23602  adjlnop  23620  adjmul  23626  adjadd  23627  branmfn  23639  kbass5  23654  kbass6  23655  leop2  23658  leopadd  23666  leopmuli  23667  pjimai  23710  atcvatlem  23919  chirredlem2  23925  mdsymlem3  23939  mdsymlem5  23941  sumdmdii  23949  sumdmdlem  23952  cdj3lem2a  23970  cdj3lem2b  23971  cdj3lem3a  23973  cdj3i  23975  xreceu  24199  toslub  24222  tosglb  24223  xrstos  24232  hasheuni  24506  ballotlemirc  24820  txpcon  24950  cvmscld  24991  2cprodeq2dv  25282  dfrdg2  25454  wsuclem  25607  nobndlem8  25685  brbtwn2  25875  ax5seglem1  25898  ax5seglem2  25899  axcontlem4  25937  segconeu  25976  linecom  26115  linethru  26118  lineintmo  26122  heicant  26277  mblfinlem1  26279  mblfinlem3  26281  ismblfin  26283  cnambfre  26291  itg2addnclem2  26295  ftc1anclem1  26318  ftc1anclem5  26322  ftc1anclem6  26323  ftc2nc  26327  areacirclem2  26331  areacirclem4  26333  areacirclem5  26334  areacirc  26335  fnemeet2  26434  fnejoin2  26436  fzmul  26482  subspopn  26496  isbndx  26529  isbnd2  26530  isbnd3  26531  ssbnd  26535  prdstotbnd  26541  heibor1  26557  rrnmet  26576  rngonegmn1l  26603  rngohomco  26628  rngoisocnv  26635  rngoisoco  26636  crngohomfo  26654  isidlc  26663  rngoidl  26672  prnc  26715  ispridlc  26718  oddcomabszz  27045  acongtr  27081  rpnnen3lem  27140  islssfg  27183  lmhmfgsplit  27199  unxpwdom3  27271  islindf3  27311  hbtlem7  27344  sdrgacs  27524  hashgcdeq  27532  dvconstbi  27566  ioovolcl  27756  2if2  28091  otsndisj  28104  ralxfrd2  28111  elovmpt3rab1  28131  elfz0fzfz0  28161  elfzonelfzo  28179  el2fzo  28185  swrdswrd  28257  usg2wlkeq  28366  usgra2pthlem1  28372  wwlknimp  28393  3cyclfrgrarn1  28500  3cyclfrgrarn  28501  4cycl2vnunb  28505  frgrancvvdeqlemB  28525  usgreghash2spotv  28553  2spotmdisj  28555  bnj1204  29479  cvrval2  30170  glbconxN  30273  hlrelat5N  30296  cvratlem  30316  cvrat2  30324  athgt  30351  3dim2  30363  llnn0  30411  lplnn0N  30442  lvoln0N  30486  snatpsubN  30645  paddasslem18  30732  pmod1i  30743  lhpexle2  30905  lhpexle3lem  30906  lhpexle3  30907  ldilcnv  31010  trlcnv  31060  trlnidatb  31072  cdleme32snaw  31330  cdleme32fvaw  31334  cdleme42ke  31380  cdlemeg46gf  31428  cdleme50trn12  31447  cdlemg1cex  31483  cdlemb3  31501  tgrpgrplem  31644  tgrpabl  31646  tendoplcl2  31673  tendo0pl  31686  tendoicl  31691  tendoipl  31692  cdlemkid3N  31828  tendoex  31870  erngdvlem4  31886  erngdvlem4-rN  31894  dib1dim  32061  dib1dim2  32064  dihglbcpreN  32196  dihmeetALTN  32223  dih1dimatlem  32225  dihatlat  32230
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator