Theorem simpl 107

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

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-ia1 104

This theorem is referenced by:  simpli  109  simpld  110  imp  122  adantrd  273  iba  294  pm3.41  324  pm4.45im  327  prth  336  pm4.71  381  adantlr  460  adantrr  462  adantllr  464  adantlrr  466  adantrlr  468  adantrrr  470  simplll  499  simplrl  501  simprll  503  simprrl  505  anabs1  536  jcab  567  pm4.38  569  pm5.21  643  ioran  701  pm3.14  702  pm4.44  728  ordi  762  pm4.39  768  pm5.16  770  pm5.54dc  860  intnanr  872  intnanrd  874  dcan  875  dedlema  910  dedlemb  911  pm4.42r  912  prlem2  915  simp1l  962  simp2l  964  simp3l  966  3anandis  1278  xordc1  1324  anxordi  1331  falantru  1334  19.26  1410  exsimpl  1548  sbequ2  1692  sbcof2  1731  sbequilem  1759  sbequ8  1768  euan  1997  mooran1  2013  eupickbi  2023  2exeu  2033  dimatis  2058  rexim  2455  r19.26  2485  r19.40  2508  rr19.28v  2734  elrab3t  2748  eueq3dc  2766  mosubt  2769  reu6  2781  sbc2iegf  2884  sbcralt  2890  sbcrext  2891  rmob  2906  csbiebt  2942  ssab2  3078  difdif  3097  uneqin  3215  indifdir  3220  undif3ss  3225  rexm  3340  difsn  3523  opprc1  3592  unissel  3630  ssmin  3655  abssexg  3955  opelopabsb  4015  sess1  4092  ordelord  4136  onin  4141  suctr  4176  ordtriexmidlem  4263  ordtri2or2exmid  4314  tfi  4323  peano1  4335  peano2  4336  0nelxp  4390  0nelelxp  4391  brab2a  4411  mosubopt  4423  posng  4430  opabssxp  4432  ideqg  4505  relssres  4666  trin2  4736  dminss  4758  iota4an  4906  iota2  4913  fun11uni  4989  imadiflem  4998  funimaexg  5003  fneq12  5012  fvelrnb  5242  dffo4  5336  ffnfv  5344  ffvresb  5349  fmptco  5351  fcoconst  5355  fcof1  5443  isotr  5476  isopolem  5481  f1oiso  5485  acexmidlemcase  5527  ovprc1  5561  fnoprabg  5622  op1steq  5825  1stconst  5862  f1o2ndf1  5869  sprmpt2  5880  brtpos2  5889  tpostpos  5902  tposf12  5907  smores  5930  tfrlemi1  5969  freceq1  6002  freceq2  6003  frectfr  6008  omv2  6068  omsuc  6074  nnsucelsuc  6093  nntri3  6098  nnaordi  6104  nnmordi  6112  nnm00  6125  ecexr  6134  ertr  6144  swoer  6157  erth  6173  ecelqsdm  6199  iinerm  6201  ecinxp  6204  erovlem  6221  dom3  6279  phpelm  6352  nnwetri  6382  supubti  6412  supisoex  6422  ordiso2  6446  dmaddpqlem  6567  distrnqg  6577  ltanqi  6592  ltmnqi  6593  ltaddnq  6597  ltrnqg  6610  ltnnnq  6613  enq0sym  6622  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  distrnq0  6649  prarloclemn  6689  prarloc  6693  ltdfpr  6696  genplt2i  6700  addnqprl  6719  addnqpru  6720  nqprl  6741  appdivnq  6753  1idprl  6780  1idpru  6781  ltexpri  6803  recexpr  6828  cauappcvgprlemdisj  6841  archrecpr  6854  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  0idsr  6944  1idsr  6945  archsr  6958  prsradd  6962  prsrlt  6963  caucvgsr  6978  elrealeu  6998  muladd11r  7264  negeu  7299  pncan  7314  pncan3  7316  negsub  7356  addid0  7477  posdif  7559  ltnegcon1  7567  subge0  7579  suble0  7580  lesub0  7583  reapval  7676  reapneg  7697  ap0gt0  7738  recextlem1  7741  div0ap  7790  recrecap  7797  rec11ap  7798  recgt0  7928  mulgt1  7941  lerec2  7967  recp1lt1  7977  recreclt  7978  ledivp1  7981  negiso  8033  nnsub  8077  avglt1  8269  nnrecl  8286  nnnn0addcl  8318  elnn0nn  8330  nn0ge2m1nn  8348  zaddcl  8391  eluzadd  8647  divfnzn  8706  qaddcl  8720  qreccl  8727  cnref1o  8733  ge0p1rp  8765  divlt1lt  8801  divle1le  8802  addlelt  8839  xrre3  8889  xltnegi  8902  ixxssixx  8925  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  zltaddlt1le  9028  elfz2  9036  peano2fzr  9056  fzdcel  9059  fzsplit2  9069  fzaddel  9077  fzrev2  9102  fzrev2i  9103  fzrev3  9104  elfz1b  9107  fseq1p1m1  9111  uzsubfz0  9140  fzosubel3  9205  eluzgtdifelfzo  9206  fzofzp1b  9237  elfzomelpfzo  9240  exfzdc  9249  fvinim0ffz  9250  qbtwnxr  9266  ico0  9270  flqge  9284  flqlt  9285  flqltnz  9289  flqbi2  9293  flqaddz  9299  flqmulnn0  9301  intfracq  9322  flqdiv  9323  q0mod  9357  q1mod  9358  mulp1mod1  9367  q2txmodxeq0  9386  modfzo0difsn  9397  frec2uzuzd  9404  frec2uzltd  9405  frec2uzrand  9407  iseqsplit  9458  iseqcaopr  9462  expivallem  9477  expival  9478  expinnval  9479  exp1  9482  expcl2lemap  9488  rpexpcl  9495  expnegzap  9510  mulexp  9515  mulexpzap  9516  leexp2r  9530  leexp1a  9531  sq11  9548  subsq  9581  binom2  9585  binom3  9590  zesq  9591  bernneq  9593  sq11ap  9639  facwordi  9667  facubnd  9672  facavg  9673  bcval  9676  ibcval5  9690  shftfvalg  9706  ovshftex  9707  shftdm  9710  shftfib  9711  shftval  9713  shftf  9718  crre  9744  cjexp  9780  cjreim2  9791  uzin2  9873  rexuz3  9876  resqrexlemgt0  9906  resqrex  9912  sqrtgt0  9920  sqrtsq  9930  sqrtmsq  9931  absrpclap  9947  absext  9949  absmul  9955  absid  9957  absexp  9965  nn0abscl  9971  abslt  9974  absle  9975  recvalap  9983  abstri  9990  caubnd2  10003  qdenre  10088  maxabsle  10090  maxabslemval  10094  maxcl  10096  rexanre  10106  min1inf  10113  climconst2  10130  climmpt  10139  climres  10142  climcaucn  10188  sumeq1  10192  dvdsdc  10203  iddvdsexp  10219  dvdsadd  10238  dvds1  10253  odd2np1  10272  oddm1even  10274  m1exp1  10301  divalglemnn  10318  fldivndvdslt  10335  flodddiv4lt  10336  zsupcllemex  10342  infssuzcldc  10347  dvdsbnd  10348  gcdnncl  10359  zeqzmulgcd  10362  gcdneg  10373  modgcd  10382  bezoutlemex  10390  bezoutlemeu  10396  dfgcd3  10399  gcdzeq  10411  dvdssq  10420  eucalgval2  10435  eucialgcvga  10440  lcmval  10445  gcddvdslcm  10455  lcmneg  10456  coprmgcdb  10470  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  cncongrcoprm  10488  prmind2  10502  dvdsnprmd  10507  exprmfct  10519  isprm6  10526  pw2dvdslemn  10543  oddpwdclemdc  10551  sqrt2irraplemnn  10557  bj-indind  10727  bj-omtrans  10751  bj-inf2vnlem1  10765  sscoll2  10783  qdencn  10785