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

Theorem simp2d 970
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp2d  |-  ( ph  ->  ch )

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp2 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
31, 2syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp2bi  973  oeeui  6837  erinxp  6970  resixp  7089  domssex  7260  cantnflem1a  7631  cantnflem1d  7634  cantnflem3  7637  cantnflem4  7638  fpwwe2lem7  8501  canthnumlem  8513  canthp1lem2  8518  wun0  8583  supmullem2  9965  supmul  9966  ixxdisj  10921  ixxun  10922  ixxss1  10924  ixxss2  10925  ixxss12  10926  ixxub  10927  ixxlb  10928  ubioo  10938  iccss2  10971  icodisj  11012  xov1plusxeqvd  11031  fldiv  11231  immul  11931  sqrge0  12053  sqrrege0  12159  icco1  12324  ruclem2  12821  ruclem3  12822  ruclem8  12826  ruclem12  12830  gcddvds  13005  crt  13157  phimullem  13158  eulerthlem1  13160  eulerthlem2  13161  prmreclem3  13276  sectcan  13971  sectco  13972  sectmon  13993  monsect  13994  funcixp  14054  funcsect  14059  invfuc  14161  coapm  14216  catciso  14252  posasymb  14399  ipodrsima  14581  pstr2  14627  psdmrn  14629  psref  14630  mhmlin  14735  subm0cl  14742  eqger  14980  eqgcpbl  14984  gaorber  15075  orbstafun  15078  cayleyth  15103  dfod2  15190  sylow2blem1  15244  dprdf  15554  dprdff  15560  dprdfcl  15561  dprdsplit  15596  dpjcntz  15600  ablfac1a  15617  ablfac1b  15618  lmodvsdi  15963  lbssp  16141  2idlcpbl  16295  assarng  16370  pnfnei  17274  cnptop2  17297  lmcl  17351  lmcnp  17358  flimfil  17991  tlmlmod  18208  ustbasel  18226  ustincl  18227  ustinvel  18229  ustfilxp  18232  tusunif  18289  imasdsf1olem  18393  xmeter  18453  tmsds  18504  metustexhalfOLD  18583  metustexhalf  18584  nlmlmod  18704  qdensere  18794  blcvx  18819  tgqioo  18821  icccmplem2  18844  reconnlem1  18847  cnmpt2pc  18943  phtpcer  19010  phtpcco2  19014  pcohtpylem  19034  pcohtpy  19035  pcophtb  19044  om1addcl  19048  pi1blem  19054  pi1cpbl  19059  pi1grplem  19064  pi1inv  19067  pi1xfrf  19068  pi1xfr  19070  pi1xfrcnvlem  19071  pi1cof  19074  pi1coghm  19076  cphnlm  19125  cphsqrcl2  19139  tchcph  19184  lmcau  19255  bcthlem4  19270  minveclem4c  19316  minveclem2  19317  minveclem3b  19319  minveclem4  19323  minveclem6  19325  ivthicc  19345  ovolfsval  19357  ovollb2lem  19374  ovolshftlem1  19395  ovolscalem1  19399  ovolicc1  19402  ovolicc2lem2  19404  ovolicc2lem4  19406  ovolicc2lem5  19407  ovolicopnf  19410  ioombl1lem1  19442  ioombl1lem3  19444  ioombl1lem4  19445  uniioovol  19461  uniioombllem2a  19464  uniioombllem2  19465  uniioombllem3a  19466  uniioombllem3  19467  uniioombllem4  19468  uniioombllem6  19470  dyadmaxlem  19479  volivth  19489  vitalilem2  19491  vitalilem5  19494  i1frn  19559  itg2monolem1  19632  itgcnlem  19671  itgrevallem1  19676  itgreval  19678  itgle  19691  ibladd  19702  iblabslem  19709  itgspliticc  19718  itgsplitioo  19719  ditgcl  19735  ditgswap  19736  ditgsplitlem  19737  limcdif  19753  limcresi  19762  limccnp  19768  limccnp2  19769  limcco  19770  dvlip  19867  dvlip2  19869  dveq0  19874  dvgt0lem1  19876  dvivthlem1  19882  dvcnvrelem1  19891  dvcnvre  19893  dvfsumlem2  19901  ftc1lem1  19909  ftc1a  19911  ftc1lem4  19913  ftc2ditglem  19919  itgsubstlem  19922  mpff  19952  mpfaddcl  19953  mpfmulcl  19954  mpfind  19955  pf1rcl  19959  mpfpf1  19961  ply1rem  20076  fta1glem1  20078  ig1pdvds  20089  plyrem  20212  facth  20213  fta1lem  20214  vieta1lem1  20217  vieta1lem2  20218  aaliou3lem3  20251  aaliou3lem4  20253  aaliou3lem7  20256  taylfvallem1  20263  tayl0  20268  taylply2  20274  radcnvle  20326  psercnlem2  20330  psercnlem1  20331  psercn  20332  pserdvlem1  20333  pserdvlem2  20334  abelth2  20348  coseq00topi  20400  coseq0negpitopi  20401  cosordlem  20423  tanord1  20429  efif1olem1  20434  loglesqr  20632  logreclem  20650  chordthmlem4  20666  quart1  20686  quartlem2  20688  quartlem3  20689  quartlem4  20690  quart  20691  acosbnd  20730  atancj  20740  atanlogsublem  20745  atantan  20753  atanbndlem  20755  dvatan  20765  atantayl  20767  rlimcnp2  20795  divsqrsumlem  20808  ftalem5  20849  ftalem7  20851  basellem4  20856  basellem5  20857  perfectlem2  21004  dchrinv  21035  chpdifbndlem1  21237  pntibndlem2  21275  pntlemc  21279  pntlema  21280  pntlemb  21281  pntlemg  21282  pntlemh  21283  pntlemq  21285  pntlemr  21286  pntlemj  21287  pntlemi  21288  pntlemf  21289  pntlemk  21290  pntlemo  21291  pntleme  21292  pntlem3  21293  pntleml  21295  abvcxp  21299  wlkonwlk  21525  constr3pth  21637  eupaf1o  21682  grpoass  21781  vcsm  22018  nvf  22137  ssps  22219  minvecolem2  22367  minvecolem4c  22371  minvecolem4  22372  minvecolem5  22373  minvecolem6  22374  eigvec1  23455  iccgelb  24126  eliccelico  24130  elicoelioo  24131  cnre2csqlem  24298  lmxrge0  24327  rnlogbval  24390  nnlogbexp  24394  sigaclci  24505  difelsiga  24506  insiga  24510  measvnul  24550  sibfrn  24642  subfacp1lem2a  24856  subfacp1lem3  24858  subfacp1lem4  24859  subfacp1lem5  24860  sconpht2  24915  sconpi1  24916  rescon  24923  cvmsss  24944  cvmsn0  24945  cvmlift2lem3  24982  cvmlift2lem7  24986  cvmliftphtlem  24994  cvmliftpht  24995  cvmlift3lem5  25000  cvmlift3lem6  25001  ghomgrplem  25090  ghomfo  25092  ghomgsg  25094  ibladdnc  26225  iblabsnclem  26231  ftc1cnnclem  26241  ivthALT  26292  heiborlem3  26476  iccbnd  26503  rngohom1  26538  idl0cl  26582  maxidlnr  26606  pmtrfinv  27334  stoweidlem11  27691  stoweidlem31  27711  stoweidlem36  27716  stoweidlem38  27718  stoweidlem44  27724  stoweidlem62  27742  sigardiv  27782  sigarcol  27785  sharhght  27786  sigaradd  27787  cevathlem1  27788  cevathlem2  27789  cevath  27790  lshpne  29681  opococ  29894  opexmid  29906  hlclat  30057  lclkrslem2  32237
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