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	⊢ ((𝜑 ∧ 𝜓) → 𝜑)

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-ia1 106	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)

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  533  simplrl  535  simprll  537  simprrl  539  anabs1  572  jcab  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2915  rr19.28v  2944  elrab3t  2959  eueq3dc  2978  mosubt  2981  reu6  2993  sbc2iegf  3100  sbcralt  3106  sbcrext  3107  rmob  3123  csbiebt  3165  ssab2  3309  difdif  3330  uneqin  3456  indifdir  3461  undif3ss  3466  rexm  3592  eqifdc  3640  ifandc  3644  ifnebibdc  3649  difsn  3808  opprc1  3882  unissel  3920  ssmin  3945  abssexg  4270  undifexmid  4281  pwntru  4287  exmidundif  4294  exmidundifim  4295  opelopabsb  4352  elopabran  4376  sess1  4432  ordelord  4476  onin  4481  suctr  4516  abnexg  4541  ifexg  4580  ordtriexmidlem  4615  ordtri2or2exmid  4667  ontri2orexmidim  4668  tfi  4678  peano1  4690  peano2  4691  nnpredcl  4719  0nelxp  4751  0nelelxp  4752  brab2a  4777  mosubopt  4789  posng  4796  opabssxp  4798  ideqg  4879  relssres  5049  trin2  5126  dminss  5149  iota4an  5305  iota2  5314  iotam  5316  fununfun  5370  fun11uni  5397  imadiflem  5406  funimaexg  5411  fneq12  5420  fvelrnb  5689  dffo4  5791  ffnfv  5801  ffvresb  5806  fmptco  5809  fcoconst  5814  funopsn  5825  fcof1  5919  isotr  5952  isopolem  5958  f1oiso  5962  acexmidlemcase  6008  ovprc1  6050  fnoprabg  6117  elovmporab  6217  elovmporab1w  6218  uchoice  6295  op1steq  6337  dmmpog  6369  1stconst  6381  f1o2ndf1  6388  brtpos2  6412  tpostpos  6425  tposf12  6430  smores  6453  tfrlemi1  6493  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  freceq1  6553  freceq2  6554  frectfr  6561  omv2  6628  omsuc  6635  nnsucelsuc  6654  nntri3  6660  nnaordi  6671  nnmordi  6679  nnm00  6693  ecexr  6702  ertr  6712  swoer  6725  erth  6743  ecelqsdm  6769  iinerm  6771  ecinxp  6774  erovlem  6791  pmresg  6840  resixp  6897  elixpsn  6899  mapsnf1o  6901  dom3  6944  modom  6989  mapdom1g  7028  ssenen  7032  phpelm  7048  finexdc  7087  exmidpweq  7096  nnwetri  7103  fiintim  7118  infidc  7127  ssfii  7167  fiss  7170  dcfi  7174  supubti  7192  supisoex  7202  ordiso2  7228  inl11  7258  omp1eomlem  7287  nnnninf  7319  nninfisol  7326  ctssexmid  7343  ismkvnex  7348  omniwomnimkv  7360  nninfwlpor  7367  nninfwlpoim  7372  nninfinfwlpo  7373  en2eleq  7399  en2other2  7400  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  acnrcl  7409  exmidaclem  7416  djuen  7419  djudoml  7427  netap  7466  2omotaplemst  7470  exmidapne  7472  cc1  7477  acnccim  7484  dmaddpqlem  7590  distrnqg  7600  ltanqi  7615  ltmnqi  7616  ltaddnq  7620  ltrnqg  7633  ltnnnq  7636  enq0sym  7645  addnq0mo  7660  mulnq0mo  7661  addnnnq0  7662  distrnq0  7672  prarloclemn  7712  prarloc  7716  ltdfpr  7719  genplt2i  7723  addnqprl  7742  addnqpru  7743  nqprl  7764  appdivnq  7776  1idprl  7803  1idpru  7804  ltexpri  7826  recexpr  7851  cauappcvgprlemdisj  7864  archrecpr  7877  addsrmo  7956  mulsrmo  7957  addsrpr  7958  mulsrpr  7959  0idsr  7980  1idsr  7981  archsr  7995  prsradd  7999  prsrlt  8000  caucvgsr  8015  map2psrprg  8018  elrealeu  8042  muladd11r  8328  negeu  8363  pncan  8378  pncan3  8380  negsub  8420  addid0  8545  posdif  8628  ltnegcon1  8636  subge0  8648  suble0  8649  lesub0  8652  reapval  8749  reapneg  8770  ap0gt0  8813  aprcl  8819  lt0ap0  8821  recextlem1  8824  recapb  8844  div0ap  8875  recrecap  8882  rec11ap  8883  recgt0  9023  mulgt1  9036  lerec2  9062  recp1lt1  9072  recreclt  9073  ledivp1  9076  negiso  9128  nnsub  9175  avglt1  9376  nnrecl  9393  nnnn0addcl  9425  elnn0nn  9437  nn0ge2m1nn  9455  zaddcl  9512  eluzmn  9755  eluzadd  9778  infregelbex  9825  divfnzn  9848  qaddcl  9862  qreccl  9869  cnref1o  9878  ge0p1rp  9913  divlt1lt  9952  divle1le  9953  addlelt  9996  xrre3  10050  xltnegi  10063  xaddval  10073  xaddcom  10089  xnegdi  10096  xposdif  10110  ixxssixx  10130  iccshftr  10222  iccshftl  10224  iccdil  10226  icccntr  10228  zltaddlt1le  10235  elfz2  10243  peano2fzr  10265  fzdcel  10268  fzsplit2  10278  fzaddel  10287  fzrev2  10313  fzrev2i  10314  fzrev3  10315  elfz1b  10318  fseq1p1m1  10322  uzsubfz0  10357  fzosubel3  10434  eluzgtdifelfzo  10435  fzofzp1b  10466  elfzomelpfzo  10469  exfzdc  10479  fvinim0ffz  10480  zsupcllemex  10483  infssuzcldc  10488  exbtwnzlemshrink  10501  qbtwnz  10504  qbtwnxr  10510  ico0  10514  elicore  10519  xqltnle  10520  apbtwnz  10527  flqge  10535  flqlt  10536  flqltnz  10540  flqbi2  10544  flqaddz  10550  flqmulnn0  10552  intfracq  10575  flqdiv  10576  q0mod  10610  q1mod  10611  mulp1mod1  10620  q2txmodxeq0  10639  modfzo0difsn  10650  frec2uzuzd  10657  frec2uzltd  10658  frec2uzrand  10660  uzennn  10691  seqfveq2g  10732  seq3split  10743  seqsplitg  10744  seq3caopr  10750  seqcaoprg  10751  seqf1oglem2  10775  seqf1og  10776  exp3vallem  10795  exp3val  10796  expnnval  10797  exp1  10800  expcl2lemap  10806  rpexpcl  10813  expnegzap  10828  mulexp  10833  mulexpzap  10834  leexp2r  10848  leexp1a  10849  sq11  10867  subsq  10901  binom2  10906  binom3  10912  zesq  10913  bernneq  10915  sq11ap  10962  zzlesq  10963  mulsubdivbinom2ap  10966  apexp1  10973  facwordi  10995  facubnd  11000  facavg  11001  bcval  11004  bcval5  11018  hashennn  11035  fihashf1rn  11043  fseq1hash  11057  hashdifsn  11076  hashdifpr  11077  hashxp  11083  fiubz  11086  fiubnn  11087  fnfz0hash  11089  ffzo0hash  11091  hash2en  11100  wrdval  11109  ffz0iswrdnn0  11133  wrdsymb0  11139  ccatsymb  11172  ccatval21sw  11175  lswccatn0lsw  11181  ccatalpha  11183  ccatrcl1  11184  s111  11201  ccat1st1st  11211  lswccats1fst  11214  swrdlen2  11236  swrdfv2  11237  swrdsbslen  11240  swrds1  11242  ccatswrd  11244  pfxval  11248  pfxclg  11252  pfxmpt  11254  pfxid  11260  pfxfv0  11266  pfxtrcfv0  11268  pfxfvlsw  11269  pfxeq  11270  ccatpfx  11275  swrdpfx  11281  lenrevpfxcctswrd  11286  wrdeqs1cat  11294  cats1un  11295  swrdccatin1  11299  pfxccatin12lem2a  11301  pfxccatin12lem1  11302  pfxccatin12lem3  11306  pfxccatin12  11307  swrdccat  11309  pfxccat3a  11312  swrdccat3blem  11313  swrdccat3b  11314  reuccatpfxs1lem  11320  reuccatpfxs1  11321  s2cl  11359  s2fv0g  11361  shftfvalg  11372  ovshftex  11373  shftdm  11376  shftfib  11377  shftval  11379  shftf  11384  crre  11411  cjexp  11447  cjreim2  11458  uzin2  11541  rexuz3  11544  resqrexlemgt0  11574  resqrex  11580  sqrtgt0  11588  sqrtsq  11598  sqrtmsq  11599  absrpclap  11615  absext  11617  absmul  11623  absid  11625  absexp  11633  nn0abscl  11639  abslt  11642  absle  11643  recvalap  11651  abstri  11658  caubnd2  11671  qdenre  11756  maxabsle  11758  maxabslemval  11762  maxcl  11764  rexanre  11774  min1inf  11786  minabs  11790  minclpr  11791  mul0inf  11795  mingeb  11796  xrmaxiflemcl  11799  xrnegiso  11816  climconst2  11845  climmpt  11854  climres  11857  climcaucn  11905  sumeq1  11909  summodclem2a  11935  isumz  11943  fisumss  11946  fsumzcl2  11959  sumsnf  11963  isumclim3  11977  fsum2dlemstep  11988  fisumcom2  11992  fsumconst  12008  cvgcmpub  12030  binom  12038  binom1p  12039  binom1dif  12041  bcxmas  12043  divcnv  12051  geo2lim  12070  geoisum  12071  geoisumr  12072  geoisum1  12073  mertenslemi1  12089  mertensabs  12091  prod1dc  12140  fprodconst  12174  fprodcom2fi  12180  efcllem  12213  efcj  12227  efadd  12229  efexp  12236  efgt1p2  12249  tanvalap  12262  tanval2ap  12267  tanval3ap  12268  sinadd  12290  cosadd  12291  dvdsdc  12352  iddvdsexp  12369  dvdsadd  12390  dvds1  12407  odd2np1  12427  oddm1even  12429  m1exp1  12455  divalglemnn  12472  fldivndvdslt  12491  flodddiv4lt  12492  bitsp1  12505  bitsmod  12510  bitsfi  12511  bitscmp  12512  bitsinv1lem  12515  dvdsbnd  12520  gcdnncl  12531  zeqzmulgcd  12534  gcdneg  12546  modgcd  12555  bezoutlemex  12565  bezoutlemeu  12571  dfgcd3  12574  gcdzeq  12586  dvdssq  12595  algrf  12610  eucalgval2  12618  eucalgcvga  12623  lcmval  12628  gcddvdslcm  12638  lcmneg  12639  coprmgcdb  12653  qredeu  12662  divgcdcoprm0  12666  divgcdcoprmex  12667  cncongr1  12668  cncongr2  12669  cncongrcoprm  12671  prmind2  12685  dvdsnprmd  12690  exprmfct  12703  isprm6  12712  pw2dvdslemn  12730  oddpwdclemdc  12738  sqrt2irraplemnn  12744  divnumden  12761  divdenle  12762  nn0sqrtelqelz  12771  phivalfi  12777  crth  12789  eulerth  12798  prmdivdiv  12802  reumodprminv  12819  nnnn0modprm0  12821  nnoddn2prmb  12828  pcval  12862  pcidlem  12889  pcid  12890  pcneg  12891  pc2dvds  12896  pcz  12898  pcprod  12912  prmpwdvds  12921  4sqexercise1  12964  2expltfac  13005  xpct  13010  znnen  13012  ennnfonelemg  13017  ennnfone  13039  ctinfom  13042  ctinf  13044  ssomct  13059  isstruct2im  13085  isstruct2r  13086  setsvalg  13105  setsslnid  13127  ressvalsets  13140  ressex  13141  2strbasg  13196  2stropg  13197  2strbas1g  13199  ressmulrg  13221  ressscag  13259  ressvscag  13260  ressipg  13261  restval  13321  restid2  13324  prdsex  13345  pwsval  13367  qusex  13401  fnpr2o  13415  xpsfval  13424  xpsval  13428  intopsn  13443  mgmidmo  13448  lidrididd  13458  ismnddef  13494  mndinvmod  13521  imasmnd2  13528  ismhm  13537  mhmex  13538  insubm  13561  dfgrp2  13603  grpsubval  13622  grpinvinv  13643  grpsubrcan  13657  grpsubadd  13664  grpaddsubass  13666  grpsubsub4  13669  grppnpcan2  13670  grpnpncan  13671  grpnpncan0  13672  grpnnncan2  13673  dfgrp3m  13675  dfgrp3me  13676  imasgrp2  13690  mhmmnd  13696  mulgfvalg  13701  mulgval  13702  mulgfng  13704  mulg1  13709  mulgnnp1  13710  mulgnndir  13731  mulgass  13739  mulgmodid  13741  issubg2m  13769  grpissubg  13774  isnsg  13782  isnsg3  13787  0nsg  13794  eqgfval  13802  eqger  13804  eqgen  13807  eqgcpbl  13808  quseccl  13813  isghm  13823  kerf1ghm  13854  conjghm  13856  conjsubg  13857  abladdsub  13895  ablpncan3  13897  ablsubsub23  13905  invghm  13909  subgabl  13912  mgpress  13937  rngdi  13946  rnglz  13951  imasrng  13962  srgmulgass  13995  srgrmhm  14000  isring  14006  ringo2times  14034  ringrng  14042  ringlz  14049  imasring  14070  opprrng  14083  opprrngbg  14084  opprring  14085  mulgass3  14091  dvdsrd  14101  dvdsrneg  14110  unitnegcl  14137  dvrvald  14141  dvrid  14144  dvr1  14145  dvrass  14146  dvrdir  14150  ringinvdv  14152  rhmex  14164  isrim0  14168  rhmval  14180  rhmdvdsr  14182  rhmopp  14183  elrhmunit  14184  rhmunitinv  14185  isnzr2  14191  ringelnzr  14194  issubrng2  14217  issubrg2  14248  aprap  14293  lmodvs1  14323  lmod0vs  14328  lmodvs0  14329  lmodvsmmulgdi  14330  lmodfopne  14333  lmodvneg1  14337  lss1  14369  islss3  14386  lsslss  14388  lss1d  14390  lspf  14396  lspsn  14423  lspsnneg  14427  sraval  14444  sraring  14456  qus1  14533  qusrhm  14535  cnfldui  14596  dvdsrzring  14610  mulgghm2  14615  mulgrhm  14616  znval  14643  znf1o  14658  psrbagfi  14680  psrplusgg  14685  mplgrpfi  14713  eltg2b  14771  difopn  14825  ntrcls0  14848  neii1  14864  restbasg  14885  resttopon  14888  restuni2  14894  cnrest2r  14954  tx1cn  14986  txcnp  14988  txcn  14992  txswaphmeo  15038  psmettri  15047  xmeteq0  15076  xmettri  15089  metrtri  15094  ssblex  15148  xmeter  15153  isxms2  15169  cnbl0  15251  cnblcld  15252  reopnap  15263  tgioo  15271  addcncntoplem  15278  expcn  15286  rescncf  15298  cncfcdm  15299  mulc1cncf  15306  cncfcncntop  15310  addccncf  15317  cdivcncfap  15321  negcncf  15322  cnopnap  15328  suplociccex  15342  hoverlt1  15366  hovergt0  15367  dich0  15369  limccl  15376  ellimc3apf  15377  cnplimcim  15384  limccnp2lem  15393  reldvg  15396  dvbsssg  15403  dvcjbr  15425  dvcj  15426  dvfre  15427  dvrecap  15430  dvef  15444  plyaddcl  15471  plymulcl  15472  plysubcl  15473  plyrecj  15480  reeff1olem  15488  pilem3  15500  ptolemy  15541  rplogcl  15596  rpcxpef  15611  cxprec  15627  rpcxproot  15631  rplogb1  15665  logbgt0b  15683  logbgcd1irr  15684  binom4  15696  wilthlem1  15697  sgmnncl  15705  dvdsppwf1o  15706  mersenne  15714  lgslem4  15725  lgsval  15726  lgsval2lem  15732  lgsval4a  15744  lgsdir2lem3  15752  lgsdir2  15755  lgsne0  15760  lgsprme0  15764  lgsmulsqcoprm  15768  gausslemma2dlem0a  15771  gausslemma2dlem1a  15780  2lgslem1b  15811  2lgslem2  15814  2lgsoddprm  15835  struct2slots2dom  15882  structvtxval  15883  structiedg0val  15884  struct2griedg  15890  edgstruct  15908  uhgr0vb  15928  incistruhgr  15934  umgrvad2edg  16055  uspgredg2vlem  16064  uspgredg2v  16065  usgredg2v  16068  ushgredgedg  16070  ushgredgedgloop  16072  usgr0vb  16077  uhgr0vusgr  16082  edg0usgr  16091  vtxdgfval  16099  wksfval  16133  wlkpropg  16135  uspgr2wlkeq2  16177  uspgr2wlkeqi  16178  upgr2wlkdc  16186  trlsex  16196  clwwlkccatlem  16209  clwwlkng  16214  clwwlkext2edg  16231  clwwlknccat  16232  umgr2cwwkdifex  16234  clwwlknonel  16241  clwwlknonccat  16242  clwwlknonex2lem2  16247  clwwlknun  16250  eupthsg  16254  bj-nnan  16282  bj-indind  16477  bj-omtrans  16501  bj-inf2vnlem1  16515  sscoll2  16533  2omap  16544  pw1map  16546  pwtrufal  16548  sssneq  16553  pw1nct  16554  nninfsellemsuc  16564  nninfomnilem  16570  nnnninfex  16574  exmidsbthrlem  16576  qdencn  16581  trilpo  16597  trirec0  16598  apdiff  16602  iswomninnlem  16603  iswomni0  16605  redcwlpo  16609  redc0  16611  reap0  16612  cndcap  16613  dceqnconst  16614  dcapnconst  16615  neapmkv  16622  neap0mkv  16623