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  277  iba  298  pm3.41  329  pm4.45im  332  anim12  342  pm4.71  387  adantlr  469  adantrr  471  adantllr  473  adantlrr  475  adantrlr  477  adantrrr  479  simplll  523  simplrl  525  simprll  527  simprrl  529  anabs1  562  jcab  593  pm4.38  595  pm5.21  685  ioran  742  pm3.14  743  pm4.44  769  ordi  806  pm4.39  812  animorl  813  animorlr  815  pm5.16  818  pm5.54dc  908  intnanr  920  intnanrd  922  dcan  923  dedlema  959  dedlemb  960  pm4.42r  961  prlem2  964  simp1l  1011  simp2l  1013  simp3l  1015  3anandis  1337  xordc1  1383  anxordi  1390  falantru  1393  19.26  1469  exsimpl  1605  sbequ2  1757  sbcof2  1798  sbequilem  1826  sbequ8  1835  euan  2070  mooran1  2086  eupickbi  2096  2exeu  2106  dimatis  2131  rexim  2559  r19.26  2591  r19.40  2619  rspcime  2836  rr19.28v  2865  elrab3t  2880  eueq3dc  2899  mosubt  2902  reu6  2914  sbc2iegf  3020  sbcralt  3026  sbcrext  3027  rmob  3042  csbiebt  3083  ssab2  3225  difdif  3246  uneqin  3372  indifdir  3377  undif3ss  3382  rexm  3507  eqifdc  3553  ifandc  3556  difsn  3709  opprc1  3779  unissel  3817  ssmin  3842  abssexg  4160  undifexmid  4171  pwntru  4177  exmidundif  4184  exmidundifim  4185  opelopabsb  4237  sess1  4314  ordelord  4358  onin  4363  suctr  4398  abnexg  4423  ordtriexmidlem  4495  ordtri2or2exmid  4547  ontri2orexmidim  4548  tfi  4558  peano1  4570  peano2  4571  nnpredcl  4599  0nelxp  4631  0nelelxp  4632  brab2a  4656  mosubopt  4668  posng  4675  opabssxp  4677  ideqg  4754  relssres  4921  trin2  4994  dminss  5017  iota4an  5171  iota2  5178  fun11uni  5257  imadiflem  5266  funimaexg  5271  fneq12  5280  fvelrnb  5533  dffo4  5632  ffnfv  5642  ffvresb  5647  fmptco  5650  fcoconst  5655  fcof1  5750  isotr  5783  isopolem  5789  f1oiso  5793  acexmidlemcase  5836  ovprc1  5874  fnoprabg  5939  op1steq  6144  dmmpog  6174  1stconst  6185  f1o2ndf1  6192  brtpos2  6215  tpostpos  6228  tposf12  6233  smores  6256  tfrlemi1  6296  tfr1onlembfn  6308  tfri1dALT  6315  tfrcllembfn  6321  freceq1  6356  freceq2  6357  frectfr  6364  omv2  6429  omsuc  6436  nnsucelsuc  6455  nntri3  6461  nnaordi  6472  nnmordi  6480  nnm00  6493  ecexr  6502  ertr  6512  swoer  6525  erth  6541  ecelqsdm  6567  iinerm  6569  ecinxp  6572  erovlem  6589  pmresg  6638  resixp  6695  elixpsn  6697  mapsnf1o  6699  dom3  6738  mapdom1g  6809  ssenen  6813  phpelm  6828  finexdc  6864  exmidpweq  6871  nnwetri  6877  fiintim  6890  ssfii  6935  fiss  6938  dcfi  6942  supubti  6960  supisoex  6970  ordiso2  6996  inl11  7026  omp1eomlem  7055  nnnninf  7086  nninfisol  7093  ctssexmid  7110  ismkvnex  7115  omniwomnimkv  7127  en2eleq  7147  en2other2  7148  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  djuen  7163  djudoml  7171  cc1  7202  dmaddpqlem  7314  distrnqg  7324  ltanqi  7339  ltmnqi  7340  ltaddnq  7344  ltrnqg  7357  ltnnnq  7360  enq0sym  7369  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  distrnq0  7396  prarloclemn  7436  prarloc  7440  ltdfpr  7443  genplt2i  7447  addnqprl  7466  addnqpru  7467  nqprl  7488  appdivnq  7500  1idprl  7527  1idpru  7528  ltexpri  7550  recexpr  7575  cauappcvgprlemdisj  7588  archrecpr  7601  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  0idsr  7704  1idsr  7705  archsr  7719  prsradd  7723  prsrlt  7724  caucvgsr  7739  map2psrprg  7742  elrealeu  7766  muladd11r  8050  negeu  8085  pncan  8100  pncan3  8102  negsub  8142  addid0  8267  posdif  8349  ltnegcon1  8357  subge0  8369  suble0  8370  lesub0  8373  reapval  8470  reapneg  8491  ap0gt0  8534  aprcl  8540  lt0ap0  8542  recextlem1  8544  div0ap  8594  recrecap  8601  rec11ap  8602  recgt0  8741  mulgt1  8754  lerec2  8780  recp1lt1  8790  recreclt  8791  ledivp1  8794  negiso  8846  nnsub  8892  avglt1  9091  nnrecl  9108  nnnn0addcl  9140  elnn0nn  9152  nn0ge2m1nn  9170  zaddcl  9227  eluzadd  9490  infregelbex  9532  divfnzn  9555  qaddcl  9569  qreccl  9576  cnref1o  9584  ge0p1rp  9617  divlt1lt  9656  divle1le  9657  addlelt  9700  xrre3  9754  xltnegi  9767  xaddval  9777  xaddcom  9793  xnegdi  9800  xposdif  9814  ixxssixx  9834  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  zltaddlt1le  9939  elfz2  9947  peano2fzr  9968  fzdcel  9971  fzsplit2  9981  fzaddel  9990  fzrev2  10016  fzrev2i  10017  fzrev3  10018  elfz1b  10021  fseq1p1m1  10025  uzsubfz0  10060  fzosubel3  10127  eluzgtdifelfzo  10128  fzofzp1b  10159  elfzomelpfzo  10162  exfzdc  10171  fvinim0ffz  10172  exbtwnzlemshrink  10180  qbtwnz  10183  qbtwnxr  10189  ico0  10193  elicore  10198  apbtwnz  10205  flqge  10213  flqlt  10214  flqltnz  10218  flqbi2  10222  flqaddz  10228  flqmulnn0  10230  intfracq  10251  flqdiv  10252  q0mod  10286  q1mod  10287  mulp1mod1  10296  q2txmodxeq0  10315  modfzo0difsn  10326  frec2uzuzd  10333  frec2uzltd  10334  frec2uzrand  10336  uzennn  10367  seq3split  10410  seq3caopr  10414  exp3vallem  10452  exp3val  10453  expnnval  10454  exp1  10457  expcl2lemap  10463  rpexpcl  10470  expnegzap  10485  mulexp  10490  mulexpzap  10491  leexp2r  10505  leexp1a  10506  sq11  10523  subsq  10557  binom2  10562  binom3  10568  zesq  10569  bernneq  10571  sq11ap  10618  apexp1  10627  facwordi  10649  facubnd  10654  facavg  10655  bcval  10658  bcval5  10672  hashennn  10689  fihashf1rn  10698  fseq1hash  10710  hashdifsn  10728  hashdifpr  10729  hashxp  10735  fiubz  10738  fiubnn  10739  fnfz0hash  10741  ffzo0hash  10743  shftfvalg  10756  ovshftex  10757  shftdm  10760  shftfib  10761  shftval  10763  shftf  10768  crre  10795  cjexp  10831  cjreim2  10842  uzin2  10925  rexuz3  10928  resqrexlemgt0  10958  resqrex  10964  sqrtgt0  10972  sqrtsq  10982  sqrtmsq  10983  absrpclap  10999  absext  11001  absmul  11007  absid  11009  absexp  11017  nn0abscl  11023  abslt  11026  absle  11027  recvalap  11035  abstri  11042  caubnd2  11055  qdenre  11140  maxabsle  11142  maxabslemval  11146  maxcl  11148  rexanre  11158  min1inf  11169  minabs  11173  minclpr  11174  mul0inf  11178  mingeb  11179  xrmaxiflemcl  11182  xrnegiso  11199  climconst2  11228  climmpt  11237  climres  11240  climcaucn  11288  sumeq1  11292  summodclem2a  11318  isumz  11326  fisumss  11329  fsumzcl2  11342  sumsnf  11346  isumclim3  11360  fsum2dlemstep  11371  fisumcom2  11375  fsumconst  11391  cvgcmpub  11413  binom  11421  binom1p  11422  binom1dif  11424  bcxmas  11426  divcnv  11434  geo2lim  11453  geoisum  11454  geoisumr  11455  geoisum1  11456  mertenslemi1  11472  mertensabs  11474  prod1dc  11523  fprodconst  11557  fprodcom2fi  11563  efcllem  11596  efcj  11610  efadd  11612  efexp  11619  efgt1p2  11632  tanvalap  11645  tanval2ap  11650  tanval3ap  11651  sinadd  11673  cosadd  11674  dvdsdc  11734  iddvdsexp  11751  dvdsadd  11772  dvds1  11787  odd2np1  11806  oddm1even  11808  m1exp1  11834  divalglemnn  11851  fldivndvdslt  11868  flodddiv4lt  11869  zsupcllemex  11875  infssuzcldc  11880  dvdsbnd  11885  gcdnncl  11896  zeqzmulgcd  11899  gcdneg  11911  modgcd  11920  bezoutlemex  11930  bezoutlemeu  11936  dfgcd3  11939  gcdzeq  11951  dvdssq  11960  algrf  11973  eucalgval2  11981  eucalgcvga  11986  lcmval  11991  gcddvdslcm  12001  lcmneg  12002  coprmgcdb  12016  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  cncongrcoprm  12034  prmind2  12048  dvdsnprmd  12053  exprmfct  12066  isprm6  12075  pw2dvdslemn  12093  oddpwdclemdc  12101  sqrt2irraplemnn  12107  divnumden  12124  divdenle  12125  nn0sqrtelqelz  12134  phivalfi  12140  crth  12152  eulerth  12161  prmdivdiv  12165  reumodprminv  12181  nnnn0modprm0  12183  nnoddn2prmb  12190  pcval  12224  pcidlem  12250  pcid  12251  pcneg  12252  pc2dvds  12257  pcz  12259  pcprod  12272  prmpwdvds  12281  xpct  12325  znnen  12327  ennnfonelemg  12332  ennnfone  12354  ctinfom  12357  ctinf  12359  ssomct  12374  isstruct2im  12400  isstruct2r  12401  setsvalg  12420  setsslnid  12441  ressid2  12449  ressval2  12450  2strbasg  12491  2stropg  12492  2strbas1g  12494  restval  12557  restid2  12560  eltg2b  12654  difopn  12708  ntrcls0  12731  neii1  12747  restbasg  12768  resttopon  12771  restuni2  12777  cnrest2r  12837  tx1cn  12869  txcnp  12871  txcn  12875  txswaphmeo  12921  psmettri  12930  xmeteq0  12959  xmettri  12972  metrtri  12977  ssblex  13031  xmeter  13036  isxms2  13052  cnbl0  13134  cnblcld  13135  reopnap  13138  tgioo  13146  addcncntoplem  13151  rescncf  13168  cncffvrn  13169  mulc1cncf  13176  cncfcncntop  13180  addccncf  13186  cdivcncfap  13187  negcncf  13188  cnopnap  13194  suplociccex  13203  limccl  13228  ellimc3apf  13229  cnplimcim  13236  limccnp2lem  13245  reldvg  13248  dvbsssg  13255  dvcjbr  13272  dvcj  13273  dvfre  13274  dvrecap  13277  dvef  13288  reeff1olem  13292  pilem3  13304  ptolemy  13345  rplogcl  13400  rpcxpef  13415  cxprec  13431  rpcxproot  13434  rplogb1  13466  logbgt0b  13484  logbgcd1irr  13485  binom4  13497  lgslem4  13504  lgsval  13505  lgsval2lem  13511  lgsval4a  13523  lgsdir2lem3  13531  lgsdir2  13534  lgsne0  13539  lgsprme0  13543  lgsmulsqcoprm  13547  bj-nnan  13577  bj-indind  13774  bj-omtrans  13798  bj-inf2vnlem1  13812  sscoll2  13830  pwtrufal  13837  sssneq  13842  pw1nct  13843  nninfsellemsuc  13852  nninfomnilem  13858  exmidsbthrlem  13861  qdencn  13866  trilpo  13882  trirec0  13883  apdiff  13887  iswomninnlem  13888  iswomni0  13890  redcwlpo  13894  redc0  13896  reap0  13897  dceqnconst  13898  dcapnconst  13899  neapmkv  13906