Theorem simpl 109

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 106	1 |- ( ( ph /\ ps ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-ia1 106

This theorem is referenced by:  simpli  111  simpld  112  imp  124  adantrd  279  iba  300  pm3.41  331  pm4.45im  334  anim12  344  pm4.71  389  adantlr  477  adantrr  479  adantllr  481  adantlrr  483  adantrlr  485  adantrrr  487  simplll  535  simplrl  537  simprll  539  simprrl  541  anabs1  574  jcab  607  pm4.38  609  pm5.21  702  ioran  759  pm3.14  760  pm4.44  786  ordi  823  pm4.39  829  animorl  830  animorlr  832  pm5.16  835  pm5.54dc  925  intnanr  937  intnanrd  939  dcan  941  dedlema  977  dedlemb  978  pm4.42r  979  prlem2  982  ifpdc  987  dfifp2dc  989  simp1l  1047  simp2l  1049  simp3l  1051  3anandis  1383  xordc1  1437  anxordi  1444  falantru  1447  19.26  1529  exsimpl  1665  sbequ2  1817  sbcof2  1858  sbequilem  1886  sbequ8  1895  euan  2136  mooran1  2152  eupickbi  2162  2exeu  2172  dimatis  2197  rexim  2626  r19.26  2659  r19.40  2687  rspcime  2917  rr19.28v  2946  elrab3t  2961  eueq3dc  2980  mosubt  2983  reu6  2995  sbc2iegf  3102  sbcralt  3108  sbcrext  3109  rmob  3125  csbiebt  3167  ssab2  3311  difdif  3332  uneqin  3458  indifdir  3463  undif3ss  3468  rexm  3594  eqifdc  3642  ifandc  3646  ifnebibdc  3651  difsn  3810  opprc1  3884  unissel  3922  ssmin  3947  abssexg  4272  undifexmid  4283  pwntru  4289  exmidundif  4296  exmidundifim  4297  opelopabsb  4354  elopabran  4378  sess1  4434  ordelord  4478  onin  4483  suctr  4518  abnexg  4543  ifexg  4582  ordtriexmidlem  4617  ordtri2or2exmid  4669  ontri2orexmidim  4670  tfi  4680  peano1  4692  peano2  4693  nnpredcl  4721  0nelxp  4753  0nelelxp  4754  brab2a  4779  mosubopt  4791  posng  4798  opabssxp  4800  ideqg  4881  relssres  5051  trin2  5128  dminss  5151  iota4an  5307  iota2  5316  iotam  5318  fununfun  5373  fun11uni  5400  imadiflem  5409  funimaexg  5414  fneq12  5423  fvelrnb  5693  dffo4  5795  ffnfv  5805  ffvresb  5810  fmptco  5813  fcoconst  5818  funopsn  5829  fcof1  5923  isotr  5956  isopolem  5962  f1oiso  5966  acexmidlemcase  6012  ovprc1  6054  fnoprabg  6121  elovmporab  6221  elovmporab1w  6222  uchoice  6299  op1steq  6341  dmmpog  6373  1stconst  6385  f1o2ndf1  6392  brtpos2  6416  tpostpos  6429  tposf12  6434  smores  6457  tfrlemi1  6497  tfr1onlembfn  6509  tfri1dALT  6516  tfrcllembfn  6522  freceq1  6557  freceq2  6558  frectfr  6565  omv2  6632  omsuc  6639  nnsucelsuc  6658  nntri3  6664  nnaordi  6675  nnmordi  6683  nnm00  6697  ecexr  6706  ertr  6716  swoer  6729  erth  6747  ecelqsdm  6773  iinerm  6775  ecinxp  6778  erovlem  6795  pmresg  6844  resixp  6901  elixpsn  6903  mapsnf1o  6905  dom3  6948  modom  6993  mapdom1g  7032  ssenen  7036  phpelm  7052  finexdc  7091  exmidpweq  7100  nnwetri  7107  fiintim  7122  infidc  7132  ssfii  7172  fiss  7175  dcfi  7179  supubti  7197  supisoex  7207  ordiso2  7233  inl11  7263  omp1eomlem  7292  nnnninf  7324  nninfisol  7331  ctssexmid  7348  ismkvnex  7353  omniwomnimkv  7365  nninfwlpor  7372  nninfwlpoim  7377  nninfinfwlpo  7378  en2eleq  7405  en2other2  7406  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acnrcl  7415  exmidaclem  7422  djuen  7425  djudoml  7433  netap  7472  2omotaplemst  7476  exmidapne  7478  cc1  7483  acnccim  7490  dmaddpqlem  7596  distrnqg  7606  ltanqi  7621  ltmnqi  7622  ltaddnq  7626  ltrnqg  7639  ltnnnq  7642  enq0sym  7651  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  distrnq0  7678  prarloclemn  7718  prarloc  7722  ltdfpr  7725  genplt2i  7729  addnqprl  7748  addnqpru  7749  nqprl  7770  appdivnq  7782  1idprl  7809  1idpru  7810  ltexpri  7832  recexpr  7857  cauappcvgprlemdisj  7870  archrecpr  7883  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  0idsr  7986  1idsr  7987  archsr  8001  prsradd  8005  prsrlt  8006  caucvgsr  8021  map2psrprg  8024  elrealeu  8048  muladd11r  8334  negeu  8369  pncan  8384  pncan3  8386  negsub  8426  addid0  8551  posdif  8634  ltnegcon1  8642  subge0  8654  suble0  8655  lesub0  8658  reapval  8755  reapneg  8776  ap0gt0  8819  aprcl  8825  lt0ap0  8827  recextlem1  8830  recapb  8850  div0ap  8881  recrecap  8888  rec11ap  8889  recgt0  9029  mulgt1  9042  lerec2  9068  recp1lt1  9078  recreclt  9079  ledivp1  9082  negiso  9134  nnsub  9181  avglt1  9382  nnrecl  9399  nnnn0addcl  9431  elnn0nn  9443  nn0ge2m1nn  9461  zaddcl  9518  eluzmn  9761  eluzadd  9784  infregelbex  9831  divfnzn  9854  qaddcl  9868  qreccl  9875  cnref1o  9884  ge0p1rp  9919  divlt1lt  9958  divle1le  9959  addlelt  10002  xrre3  10056  xltnegi  10069  xaddval  10079  xaddcom  10095  xnegdi  10102  xposdif  10116  ixxssixx  10136  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  zltaddlt1le  10241  elfz2  10249  peano2fzr  10271  fzdcel  10274  fzsplit2  10284  fzaddel  10293  fzrev2  10319  fzrev2i  10320  fzrev3  10321  elfz1b  10324  fseq1p1m1  10328  uzsubfz0  10363  fzosubel3  10440  eluzgtdifelfzo  10441  fzofzp1b  10472  elfzomelpfzo  10475  exfzdc  10485  fvinim0ffz  10486  zsupcllemex  10489  infssuzcldc  10494  exbtwnzlemshrink  10507  qbtwnz  10510  qbtwnxr  10516  ico0  10520  elicore  10525  xqltnle  10526  apbtwnz  10533  flqge  10541  flqlt  10542  flqltnz  10546  flqbi2  10550  flqaddz  10556  flqmulnn0  10558  intfracq  10581  flqdiv  10582  q0mod  10616  q1mod  10617  mulp1mod1  10626  q2txmodxeq0  10645  modfzo0difsn  10656  frec2uzuzd  10663  frec2uzltd  10664  frec2uzrand  10666  uzennn  10697  seqfveq2g  10738  seq3split  10749  seqsplitg  10750  seq3caopr  10756  seqcaoprg  10757  seqf1oglem2  10781  seqf1og  10782  exp3vallem  10801  exp3val  10802  expnnval  10803  exp1  10806  expcl2lemap  10812  rpexpcl  10819  expnegzap  10834  mulexp  10839  mulexpzap  10840  leexp2r  10854  leexp1a  10855  sq11  10873  subsq  10907  binom2  10912  binom3  10918  zesq  10919  bernneq  10921  sq11ap  10968  zzlesq  10969  mulsubdivbinom2ap  10972  apexp1  10979  facwordi  11001  facubnd  11006  facavg  11007  bcval  11010  bcval5  11024  hashennn  11041  fihashf1rn  11049  fseq1hash  11063  hashdifsn  11082  hashdifpr  11083  hashxp  11089  fiubz  11092  fiubnn  11093  fnfz0hash  11095  ffzo0hash  11097  hash2en  11106  wrdval  11115  ffz0iswrdnn0  11139  wrdsymb0  11145  ccatsymb  11178  ccatval21sw  11181  lswccatn0lsw  11187  ccatalpha  11189  ccatrcl1  11190  s111  11207  ccat1st1st  11217  lswccats1fst  11220  swrdlen2  11242  swrdfv2  11243  swrdsbslen  11246  swrds1  11248  ccatswrd  11250  pfxval  11254  pfxclg  11258  pfxmpt  11260  pfxid  11266  pfxfv0  11272  pfxtrcfv0  11274  pfxfvlsw  11275  pfxeq  11276  ccatpfx  11281  swrdpfx  11287  lenrevpfxcctswrd  11292  wrdeqs1cat  11300  cats1un  11301  swrdccatin1  11305  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  pfxccatin12lem3  11312  pfxccatin12  11313  swrdccat  11315  pfxccat3a  11318  swrdccat3blem  11319  swrdccat3b  11320  reuccatpfxs1lem  11326  reuccatpfxs1  11327  s2cl  11365  s2fv0g  11367  shftfvalg  11378  ovshftex  11379  shftdm  11382  shftfib  11383  shftval  11385  shftf  11390  crre  11417  cjexp  11453  cjreim2  11464  uzin2  11547  rexuz3  11550  resqrexlemgt0  11580  resqrex  11586  sqrtgt0  11594  sqrtsq  11604  sqrtmsq  11605  absrpclap  11621  absext  11623  absmul  11629  absid  11631  absexp  11639  nn0abscl  11645  abslt  11648  absle  11649  recvalap  11657  abstri  11664  caubnd2  11677  qdenre  11762  maxabsle  11764  maxabslemval  11768  maxcl  11770  rexanre  11780  min1inf  11792  minabs  11796  minclpr  11797  mul0inf  11801  mingeb  11802  xrmaxiflemcl  11805  xrnegiso  11822  climconst2  11851  climmpt  11860  climres  11863  climcaucn  11911  sumeq1  11915  summodclem2a  11941  isumz  11949  fisumss  11952  fsumzcl2  11965  sumsnf  11969  isumclim3  11983  fsum2dlemstep  11994  fisumcom2  11998  fsumconst  12014  cvgcmpub  12036  binom  12044  binom1p  12045  binom1dif  12047  bcxmas  12049  divcnv  12057  geo2lim  12076  geoisum  12077  geoisumr  12078  geoisum1  12079  mertenslemi1  12095  mertensabs  12097  prod1dc  12146  fprodconst  12180  fprodcom2fi  12186  efcllem  12219  efcj  12233  efadd  12235  efexp  12242  efgt1p2  12255  tanvalap  12268  tanval2ap  12273  tanval3ap  12274  sinadd  12296  cosadd  12297  dvdsdc  12358  iddvdsexp  12375  dvdsadd  12396  dvds1  12413  odd2np1  12433  oddm1even  12435  m1exp1  12461  divalglemnn  12478  fldivndvdslt  12497  flodddiv4lt  12498  bitsp1  12511  bitsmod  12516  bitsfi  12517  bitscmp  12518  bitsinv1lem  12521  dvdsbnd  12526  gcdnncl  12537  zeqzmulgcd  12540  gcdneg  12552  modgcd  12561  bezoutlemex  12571  bezoutlemeu  12577  dfgcd3  12580  gcdzeq  12592  dvdssq  12601  algrf  12616  eucalgval2  12624  eucalgcvga  12629  lcmval  12634  gcddvdslcm  12644  lcmneg  12645  coprmgcdb  12659  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  cncongrcoprm  12677  prmind2  12691  dvdsnprmd  12696  exprmfct  12709  isprm6  12718  pw2dvdslemn  12736  oddpwdclemdc  12744  sqrt2irraplemnn  12750  divnumden  12767  divdenle  12768  nn0sqrtelqelz  12777  phivalfi  12783  crth  12795  eulerth  12804  prmdivdiv  12808  reumodprminv  12825  nnnn0modprm0  12827  nnoddn2prmb  12834  pcval  12868  pcidlem  12895  pcid  12896  pcneg  12897  pc2dvds  12902  pcz  12904  pcprod  12918  prmpwdvds  12927  4sqexercise1  12970  2expltfac  13011  xpct  13016  znnen  13018  ennnfonelemg  13023  ennnfone  13045  ctinfom  13048  ctinf  13050  ssomct  13065  isstruct2im  13091  isstruct2r  13092  setsvalg  13111  setsslnid  13133  ressvalsets  13146  ressex  13147  2strbasg  13202  2stropg  13203  2strbas1g  13205  ressmulrg  13227  ressscag  13265  ressvscag  13266  ressipg  13267  restval  13327  restid2  13330  prdsex  13351  pwsval  13373  qusex  13407  fnpr2o  13421  xpsfval  13430  xpsval  13434  intopsn  13449  mgmidmo  13454  lidrididd  13464  ismnddef  13500  mndinvmod  13527  imasmnd2  13534  ismhm  13543  mhmex  13544  insubm  13567  dfgrp2  13609  grpsubval  13628  grpinvinv  13649  grpsubrcan  13663  grpsubadd  13670  grpaddsubass  13672  grpsubsub4  13675  grppnpcan2  13676  grpnpncan  13677  grpnpncan0  13678  grpnnncan2  13679  dfgrp3m  13681  dfgrp3me  13682  imasgrp2  13696  mhmmnd  13702  mulgfvalg  13707  mulgval  13708  mulgfng  13710  mulg1  13715  mulgnnp1  13716  mulgnndir  13737  mulgass  13745  mulgmodid  13747  issubg2m  13775  grpissubg  13780  isnsg  13788  isnsg3  13793  0nsg  13800  eqgfval  13808  eqger  13810  eqgen  13813  eqgcpbl  13814  quseccl  13819  isghm  13829  kerf1ghm  13860  conjghm  13862  conjsubg  13863  abladdsub  13901  ablpncan3  13903  ablsubsub23  13911  invghm  13915  subgabl  13918  mgpress  13943  rngdi  13952  rnglz  13957  imasrng  13968  srgmulgass  14001  srgrmhm  14006  isring  14012  ringo2times  14040  ringrng  14048  ringlz  14055  imasring  14076  opprrng  14089  opprrngbg  14090  opprring  14091  mulgass3  14097  dvdsrd  14107  dvdsrneg  14116  unitnegcl  14143  dvrvald  14147  dvrid  14150  dvr1  14151  dvrass  14152  dvrdir  14156  ringinvdv  14158  rhmex  14170  isrim0  14174  rhmval  14186  rhmdvdsr  14188  rhmopp  14189  elrhmunit  14190  rhmunitinv  14191  isnzr2  14197  ringelnzr  14200  issubrng2  14223  issubrg2  14254  aprap  14299  lmodvs1  14329  lmod0vs  14334  lmodvs0  14335  lmodvsmmulgdi  14336  lmodfopne  14339  lmodvneg1  14343  lss1  14375  islss3  14392  lsslss  14394  lss1d  14396  lspf  14402  lspsn  14429  lspsnneg  14433  sraval  14450  sraring  14462  qus1  14539  qusrhm  14541  cnfldui  14602  dvdsrzring  14616  mulgghm2  14621  mulgrhm  14622  znval  14649  znf1o  14664  psrbagfi  14686  psrplusgg  14691  mplgrpfi  14719  eltg2b  14777  difopn  14831  ntrcls0  14854  neii1  14870  restbasg  14891  resttopon  14894  restuni2  14900  cnrest2r  14960  tx1cn  14992  txcnp  14994  txcn  14998  txswaphmeo  15044  psmettri  15053  xmeteq0  15082  xmettri  15095  metrtri  15100  ssblex  15154  xmeter  15159  isxms2  15175  cnbl0  15257  cnblcld  15258  reopnap  15269  tgioo  15277  addcncntoplem  15284  expcn  15292  rescncf  15304  cncfcdm  15305  mulc1cncf  15312  cncfcncntop  15316  addccncf  15323  cdivcncfap  15327  negcncf  15328  cnopnap  15334  suplociccex  15348  hoverlt1  15372  hovergt0  15373  dich0  15375  limccl  15382  ellimc3apf  15383  cnplimcim  15390  limccnp2lem  15399  reldvg  15402  dvbsssg  15409  dvcjbr  15431  dvcj  15432  dvfre  15433  dvrecap  15436  dvef  15450  plyaddcl  15477  plymulcl  15478  plysubcl  15479  plyrecj  15486  reeff1olem  15494  pilem3  15506  ptolemy  15547  rplogcl  15602  rpcxpef  15617  cxprec  15633  rpcxproot  15637  rplogb1  15671  logbgt0b  15689  logbgcd1irr  15690  binom4  15702  wilthlem1  15703  sgmnncl  15711  dvdsppwf1o  15712  mersenne  15720  lgslem4  15731  lgsval  15732  lgsval2lem  15738  lgsval4a  15750  lgsdir2lem3  15758  lgsdir2  15761  lgsne0  15766  lgsprme0  15770  lgsmulsqcoprm  15774  gausslemma2dlem0a  15777  gausslemma2dlem1a  15786  2lgslem1b  15817  2lgslem2  15820  2lgsoddprm  15841  struct2slots2dom  15888  structvtxval  15889  structiedg0val  15890  struct2griedg  15896  edgstruct  15914  uhgr0vb  15934  incistruhgr  15940  umgrvad2edg  16061  uspgredg2vlem  16070  uspgredg2v  16071  usgredg2v  16074  ushgredgedg  16076  ushgredgedgloop  16078  usgr0vb  16083  uhgr0vusgr  16088  edg0usgr  16097  subupgr  16123  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  vtxdgfval  16138  wksfval  16172  wlkpropg  16174  uspgr2wlkeq2  16216  uspgr2wlkeqi  16217  upgr2wlkdc  16227  trlsex  16237  clwwlkccatlem  16250  clwwlkng  16255  clwwlkext2edg  16272  clwwlknccat  16273  umgr2cwwkdifex  16275  clwwlknonel  16282  clwwlknonccat  16283  clwwlknonex2lem2  16288  clwwlknun  16291  eupthsg  16295  bj-nnan  16332  bj-indind  16527  bj-omtrans  16551  bj-inf2vnlem1  16565  sscoll2  16583  2omap  16594  pw1map  16596  pwtrufal  16598  sssneq  16603  pw1nct  16604  nninfsellemsuc  16614  nninfomnilem  16620  nnnninfex  16624  exmidsbthrlem  16626  qdencn  16631  trilpo  16647  trirec0  16648  apdiff  16652  iswomninnlem  16653  iswomni0  16655  redcwlpo  16659  redc0  16661  reap0  16662  cndcap  16663  dceqnconst  16664  dcapnconst  16665  neapmkv  16672  neap0mkv  16673