Theorem simpl 108

Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
simpl	|- ( ( ph /\ ps ) -> ph )

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-ia1 105	1 |- ( ( ph /\ ps ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-ia1 105

This theorem is referenced by:  simpli  110  simpld  111  imp  123  adantrd  275  iba  296  pm3.41  327  pm4.45im  330  prth  339  pm4.71  384  adantlr  466  adantrr  468  adantllr  470  adantlrr  472  adantrlr  474  adantrrr  476  simplll  505  simplrl  507  simprll  509  simprrl  511  anabs1  544  jcab  575  pm4.38  577  pm5.21  667  ioran  724  pm3.14  725  pm4.44  751  ordi  788  pm4.39  794  pm5.16  796  pm5.54dc  886  intnanr  898  intnanrd  900  dcan  901  dedlema  936  dedlemb  937  pm4.42r  938  prlem2  941  simp1l  988  simp2l  990  simp3l  992  3anandis  1308  xordc1  1354  anxordi  1361  falantru  1364  19.26  1440  exsimpl  1579  sbequ2  1725  sbcof2  1764  sbequilem  1792  sbequ8  1801  euan  2031  mooran1  2047  eupickbi  2057  2exeu  2067  dimatis  2092  rexim  2500  r19.26  2532  r19.40  2559  rr19.28v  2794  elrab3t  2808  eueq3dc  2827  mosubt  2830  reu6  2842  sbc2iegf  2947  sbcralt  2953  sbcrext  2954  rmob  2969  csbiebt  3005  ssab2  3147  difdif  3167  uneqin  3293  indifdir  3298  undif3ss  3303  rexm  3428  eqifdc  3472  ifandc  3474  difsn  3623  opprc1  3693  unissel  3731  ssmin  3756  abssexg  4066  undifexmid  4077  pwntru  4082  exmidundif  4089  exmidundifim  4090  opelopabsb  4142  sess1  4219  ordelord  4263  onin  4268  suctr  4303  abnexg  4327  ordtriexmidlem  4395  ordtri2or2exmid  4446  tfi  4456  peano1  4468  peano2  4469  nnpredcl  4496  0nelxp  4527  0nelelxp  4528  brab2a  4552  mosubopt  4564  posng  4571  opabssxp  4573  ideqg  4650  relssres  4815  trin2  4888  dminss  4911  iota4an  5065  iota2  5072  fun11uni  5151  imadiflem  5160  funimaexg  5165  fneq12  5174  fvelrnb  5423  dffo4  5522  ffnfv  5532  ffvresb  5537  fmptco  5540  fcoconst  5545  fcof1  5638  isotr  5671  isopolem  5677  f1oiso  5681  acexmidlemcase  5723  ovprc1  5761  fnoprabg  5826  op1steq  6031  dmmpog  6061  1stconst  6072  f1o2ndf1  6079  brtpos2  6102  tpostpos  6115  tposf12  6120  smores  6143  tfrlemi1  6183  tfr1onlembfn  6195  tfri1dALT  6202  tfrcllembfn  6208  freceq1  6243  freceq2  6244  frectfr  6251  omv2  6315  omsuc  6322  nnsucelsuc  6341  nntri3  6347  nnaordi  6358  nnmordi  6366  nnm00  6379  ecexr  6388  ertr  6398  swoer  6411  erth  6427  ecelqsdm  6453  iinerm  6455  ecinxp  6458  erovlem  6475  pmresg  6524  resixp  6581  elixpsn  6583  mapsnf1o  6585  dom3  6624  mapdom1g  6694  ssenen  6698  phpelm  6713  finexdc  6749  nnwetri  6757  fiintim  6770  ssfii  6814  fiss  6817  supubti  6838  supisoex  6848  ordiso2  6872  inl11  6902  omp1eomlem  6931  nnnninf  6973  ctssexmid  6974  ismkvnex  6979  en2eleq  6999  en2other2  7000  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  exmidaclem  7012  djuen  7015  djudoml  7023  dmaddpqlem  7133  distrnqg  7143  ltanqi  7158  ltmnqi  7159  ltaddnq  7163  ltrnqg  7176  ltnnnq  7179  enq0sym  7188  addnq0mo  7203  mulnq0mo  7204  addnnnq0  7205  distrnq0  7215  prarloclemn  7255  prarloc  7259  ltdfpr  7262  genplt2i  7266  addnqprl  7285  addnqpru  7286  nqprl  7307  appdivnq  7319  1idprl  7346  1idpru  7347  ltexpri  7369  recexpr  7394  cauappcvgprlemdisj  7407  archrecpr  7420  addsrmo  7486  mulsrmo  7487  addsrpr  7488  mulsrpr  7489  0idsr  7510  1idsr  7511  archsr  7524  prsradd  7528  prsrlt  7529  caucvgsr  7544  elrealeu  7564  muladd11r  7841  negeu  7876  pncan  7891  pncan3  7893  negsub  7933  addid0  8054  posdif  8136  ltnegcon1  8144  subge0  8156  suble0  8157  lesub0  8160  reapval  8256  reapneg  8277  ap0gt0  8319  recextlem1  8325  div0ap  8375  recrecap  8382  rec11ap  8383  recgt0  8518  mulgt1  8531  lerec2  8557  recp1lt1  8567  recreclt  8568  ledivp1  8571  negiso  8623  nnsub  8669  avglt1  8862  nnrecl  8879  nnnn0addcl  8911  elnn0nn  8923  nn0ge2m1nn  8941  zaddcl  8998  eluzadd  9256  divfnzn  9315  qaddcl  9329  qreccl  9336  cnref1o  9342  ge0p1rp  9374  divlt1lt  9410  divle1le  9411  addlelt  9448  xrre3  9498  xltnegi  9511  xaddval  9521  xaddcom  9537  xnegdi  9544  xposdif  9558  ixxssixx  9578  iccshftr  9670  iccshftl  9672  iccdil  9674  icccntr  9676  zltaddlt1le  9682  elfz2  9690  peano2fzr  9710  fzdcel  9713  fzsplit2  9723  fzaddel  9732  fzrev2  9758  fzrev2i  9759  fzrev3  9760  elfz1b  9763  fseq1p1m1  9767  uzsubfz0  9799  fzosubel3  9866  eluzgtdifelfzo  9867  fzofzp1b  9898  elfzomelpfzo  9901  exfzdc  9910  fvinim0ffz  9911  exbtwnzlemshrink  9919  qbtwnz  9922  qbtwnxr  9928  ico0  9932  apbtwnz  9940  flqge  9948  flqlt  9949  flqltnz  9953  flqbi2  9957  flqaddz  9963  flqmulnn0  9965  intfracq  9986  flqdiv  9987  q0mod  10021  q1mod  10022  mulp1mod1  10031  q2txmodxeq0  10050  modfzo0difsn  10061  frec2uzuzd  10068  frec2uzltd  10069  frec2uzrand  10071  uzennn  10102  seq3split  10145  seq3caopr  10149  exp3vallem  10187  exp3val  10188  expnnval  10189  exp1  10192  expcl2lemap  10198  rpexpcl  10205  expnegzap  10220  mulexp  10225  mulexpzap  10226  leexp2r  10240  leexp1a  10241  sq11  10258  subsq  10292  binom2  10296  binom3  10302  zesq  10303  bernneq  10305  sq11ap  10351  facwordi  10379  facubnd  10384  facavg  10385  bcval  10388  bcval5  10402  hashennn  10419  fihashf1rn  10428  fseq1hash  10440  hashdifsn  10458  hashdifpr  10459  hashxp  10465  fnfz0hash  10468  ffzo0hash  10470  shftfvalg  10483  ovshftex  10484  shftdm  10487  shftfib  10488  shftval  10490  shftf  10495  crre  10522  cjexp  10558  cjreim2  10569  uzin2  10651  rexuz3  10654  resqrexlemgt0  10684  resqrex  10690  sqrtgt0  10698  sqrtsq  10708  sqrtmsq  10709  absrpclap  10725  absext  10727  absmul  10733  absid  10735  absexp  10743  nn0abscl  10749  abslt  10752  absle  10753  recvalap  10761  abstri  10768  caubnd2  10781  qdenre  10866  maxabsle  10868  maxabslemval  10872  maxcl  10874  rexanre  10884  min1inf  10895  minabs  10899  minclpr  10900  mul0inf  10904  xrmaxiflemcl  10906  xrnegiso  10923  climconst2  10952  climmpt  10961  climres  10964  climcaucn  11012  sumeq1  11016  summodclem2a  11042  isumz  11050  fisumss  11053  fsumzcl2  11066  sumsnf  11070  isumclim3  11084  fsum2dlemstep  11095  fisumcom2  11099  fsumconst  11115  cvgcmpub  11137  binom  11145  binom1p  11146  binom1dif  11148  bcxmas  11150  divcnv  11158  geo2lim  11177  geoisum  11178  geoisumr  11179  geoisum1  11180  mertenslemi1  11196  mertensabs  11198  efcllem  11216  efcj  11230  efadd  11232  efexp  11239  efgt1p2  11252  efler  11256  tanvalap  11266  tanval2ap  11271  tanval3ap  11272  sinadd  11294  cosadd  11295  dvdsdc  11349  iddvdsexp  11365  dvdsadd  11384  dvds1  11399  odd2np1  11418  oddm1even  11420  m1exp1  11446  divalglemnn  11463  fldivndvdslt  11480  flodddiv4lt  11481  zsupcllemex  11487  infssuzcldc  11492  dvdsbnd  11493  gcdnncl  11504  zeqzmulgcd  11507  gcdneg  11518  modgcd  11527  bezoutlemex  11535  bezoutlemeu  11541  dfgcd3  11544  gcdzeq  11556  dvdssq  11565  algrf  11572  eucalgval2  11580  eucalgcvga  11585  lcmval  11590  gcddvdslcm  11600  lcmneg  11601  coprmgcdb  11615  qredeu  11624  divgcdcoprm0  11628  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  cncongrcoprm  11633  prmind2  11647  dvdsnprmd  11652  exprmfct  11664  isprm6  11671  pw2dvdslemn  11688  oddpwdclemdc  11696  sqrt2irraplemnn  11702  divnumden  11719  divdenle  11720  nn0sqrtelqelz  11729  phivalfi  11733  crth  11745  xpct  11754  znnen  11756  ennnfonelemg  11761  ennnfone  11783  ctinfom  11786  ctinf  11788  isstruct2im  11812  isstruct2r  11813  setsvalg  11832  setsslnid  11853  ressid2  11861  ressval2  11862  2strbasg  11903  2stropg  11904  2strbas1g  11906  restval  11969  restid2  11972  eltg2b  12066  difopn  12120  ntrcls0  12143  neii1  12159  restbasg  12180  resttopon  12183  restuni2  12189  cnrest2r  12248  tx1cn  12280  txcnp  12282  txcn  12286  psmettri  12319  xmeteq0  12348  xmettri  12361  metrtri  12366  ssblex  12420  xmeter  12425  isxms2  12441  cnbl0  12523  cnblcld  12524  tgioo  12532  addcncntoplem  12537  rescncf  12554  cncffvrn  12555  mulc1cncf  12562  cncfcncntop  12566  addccncf  12572  cdivcncfap  12573  negcncf  12574  limccl  12584  ellimc3apf  12585  cnplimcim  12592  limccnp2lem  12601  reldvg  12603  dvbsssg  12610  bj-nnan  12641  bj-indind  12822  bj-omtrans  12846  bj-inf2vnlem1  12860  sscoll2  12878  pwtrufal  12884  nninfsellemsuc  12900  nninfomnilem  12906  exmidsbthrlem  12909  qdencn  12914  trilpo  12928