Theorem simpll 531

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
simpll	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad2antrr 492	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1ll  1091  simp2ll  1095  simp3ll  1099  rmob  3145  ifnefals  3685  ifeqeqxdc  3687  prneimg  3897  exmid01  4333  pwntru  4334  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  poinxp  4842  mpteqb  5793  fvmptt  5794  fcof1  5983  acexmid  6078  fsuppeqg  6482  fvn0elsupp  6485  suppssdc  6494  suppssfvg  6497  dftpos4  6528  tfrlem3ag  6574  tfrlem3a  6575  tfrlemi1  6597  tfrexlem  6599  tfr1onlem3ag  6602  nntr2  6770  dcdifsnid  6771  qsel  6880  ecopovsymg  6902  ecopoverg  6904  th3qlem1  6905  mapss  6967  xpmapenlem  7143  findcard2  7187  findcard2s  7188  findcard2sd  7190  unfiin  7227  f1finf1o  7258  fidcenumlemrk  7265  fidcenumlemr  7266  fidcenum  7267  sbthlemi6  7273  sbthlemi8  7275  elfi2  7300  f1setfi  7311  2omap  7312  2omapfi  7314  supisolem  7342  enumct  7449  nninfninc  7457  ismkvnex  7489  exmidontriimlem4  7574  netap  7614  2omotaplemap  7617  cc2lem  7626  dfplpq2  7715  dfmpq2  7716  mulpipqqs  7734  distrnqg  7748  ltexnqq  7769  subhalfnqq  7775  prarloclemarch  7779  nnnq0lem1  7807  distrnq0  7820  npsspw  7832  prarloclemlo  7855  prarloclem3  7858  prarloclemcalc  7863  genplt2i  7871  distrlem1prl  7943  distrlem1pru  7944  distrlem4prl  7945  distrlem4pru  7946  ltprordil  7950  ltexprlemlol  7963  ltexprlemupu  7965  addextpr  7982  recexprlemopl  7986  recexprlemdisj  7991  recexprlem1ssl  7994  aptiprleml  8000  prsrlem1  8103  recexgt0sr  8134  addcnsr  8195  mulcnsr  8196  mulcnsrec  8204  axaddcl  8225  axmulcl  8227  axmulcom  8232  rereceu  8250  mpomulf  8310  ltntri  8448  cnegexlem1  8495  cnegex  8498  addsub4  8563  le2add  8766  lt2add  8767  lt2sub  8782  le2sub  8783  rereim  8908  apreim  8925  mulreim  8926  addext  8932  mulext  8936  receuap  8993  rec11ap  9034  rec11rap  9035  divdivdivap  9037  ddcanap  9050  divadddivap  9051  divsubdivap  9052  conjmulap  9053  rerecclap  9054  subrecap  9163  recgt0  9174  prodgt0gt0  9175  prodgt0  9176  prodge0  9178  ltmul12a  9184  lemul12a  9186  lemulge11  9190  lt2mul2div  9203  ltrec  9207  lerec  9208  lt2msq  9210  ltrec1  9212  le2msq  9225  msq11  9226  ledivp1  9227  mulle0r  9268  peano5uzti  9737  eluzuzle  9913  qreccl  10025  elpq  10032  xrltso  10181  z2ge  10211  xpncan  10256  xaddge0  10263  xle2add  10264  xleaddadd  10272  ixxss1  10289  ixxss2  10290  elioc2  10321  divelunit  10387  fzass4  10451  fzrev  10474  fzonmapblen  10582  elfzodifsumelfzo  10602  ssfzo12bi  10626  rebtwn2z  10672  qbtwnxr  10675  modqid  10769  modqcyc  10779  modqaddabs  10782  modqaddmod  10783  mulqaddmodid  10784  modqadd2mod  10794  modqltm1p1mod  10796  modqsubmod  10802  modqsubmodmod  10803  modqmulmod  10809  modqmulmodr  10810  modqsubdir  10813  frecuzrdgg  10836  nninfinf  10863  seq3val  10880  seqvalcd  10881  seq3feq  10900  seq3f1olemp  10935  seqfeq4g  10951  expp1  10966  expcl2lemap  10971  expnegzap  10993  expadd  11001  expmul  11004  leexp1a  11014  resq01  11078  expnlbnd  11085  nn0ltexp2  11130  nn0opth2  11145  bcval  11170  bcval5  11184  bcpasc  11187  hashunsng  11231  sseqn  11262  hashfibclem  11265  hashfibc  11266  hashf1lem2  11269  seq3coll  11277  iswrdiz  11294  sswrd  11296  ccatalpha  11364  ccatw2s1p1g  11396  swrdwrdsymbg  11419  swrdsb0eq  11420  ccatswrd  11425  pfxf  11437  pfxwrdsymbg  11445  wrd2ind  11478  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccatin12  11488  pfxccat3  11489  swrdccat  11490  shftfvalg  11566  shftfval  11569  seq3shft  11586  caucvgrelemrec  11728  resqrexlemdecn  11761  sqrtmul  11784  sqrtdiv  11791  leabs  11823  absexpzap  11829  ltabs  11836  abslt  11837  absle  11838  abssubap0  11839  amgm2  11867  icodiamlt  11929  qdenre  11951  maxleim  11954  maxleastlt  11964  rexico  11970  zmaxcl  11973  minmax  11979  xrmaxleastlt  12005  xrminmax  12014  climuni  12042  cn1lem  12063  iserex  12088  iserle  12091  climserle  12094  climcau  12096  summodclem2a  12131  summodc  12133  isumss  12141  fisumss  12142  fsumadd  12156  isumadd  12181  fsum2dlemstep  12184  fsum2d  12185  fisum0diag2  12197  fsumabs  12215  isumsplit  12241  geolim  12261  geo2lim  12266  geoisum  12267  geoisumr  12268  geoisum1  12269  mertenslemub  12284  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodseq  12333  fprodcl2lem  12355  fprod2dlemstep  12372  fprodle  12390  fprodmodd  12391  efcvgfsum  12417  eftlcl  12438  reeftlcl  12439  tanaddap  12489  zdvdsdc  12562  dvds2ln  12574  dvdsle  12594  divconjdvds  12599  dvdsext  12605  bitsfzo  12705  gcdsupex  12717  gcdsupcl  12718  bezoutlemmain  12758  bezoutlemaz  12763  bezoutlembi  12765  bezout  12771  gcdmultiplez  12781  dvdsmulgcd  12785  bezoutr  12792  bezoutr1  12793  lcmval  12824  lcmcllem  12828  ncoprmgcdne1b  12850  cncongr1  12864  isprm5  12903  prmdvdsexp  12909  sqrt2irr  12923  pw2dvdslemn  12926  pw2dvdseu  12929  nonsq  12968  powm2modprm  13014  pcmul  13063  pcqmul  13065  pcexp  13071  pcneg  13087  pcdvdstr  13089  pcprmpw2  13095  pcfac  13112  expnprm  13115  prmpwdvds  13117  mul4sq  13156  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemsima  13242  ssnnctlemct  13320  infpn2  13330  isstruct2r  13346  setsfun  13370  setsfun0  13371  ismndd  13733  submnd0  13740  mhmf1o  13760  resmhm  13777  mhmco  13780  mhmima  13781  dfgrp2  13815  grprcan  13825  grplmulf1o  13862  grplactcnv  13890  mhmmnd  13902  mulgval  13908  mulgz  13936  mulgnn0dir  13938  mulgdir  13940  mulgneg2  13942  mhmmulg  13949  issubg4m  13979  nmzsubg  13996  ssnmz  13997  ghmmhmb  14040  resghm  14046  ghmpreima  14052  ghmnsgpreima  14055  ghmf1o  14061  eqgabl  14117  gzsumconst  14126  pwssub  14199  rngpropd  14237  srglmhm  14280  srgrmhm  14281  isring  14287  ringadd2  14315  ringpropd  14326  ringlghm  14349  ringrghm  14350  oppr1g  14371  dvdsrex  14388  dvdsrtr  14391  issubrg  14512  unitrrg  14559  aprnzr  14582  opprdrng  14603  islmod  14610  islmodd  14612  lmodfopne  14646  lmodprop2d  14668  lssvacl  14685  lssvsubcl  14686  lssvscl  14695  islss3  14699  lsslss  14701  lss1d  14703  lsspropdg  14751  dflidl2rng  14801  expghmap  14925  mulgghm2  14926  znval  14954  znunit  14977  znrrg  14978  assapropd  14997  assamulgscmlem1  15024  assamulgscmlem2  15025  psrbaglesuppg  15040  mplvalcoe  15064  neissex  15249  tgrest  15253  ssrest  15266  restopn2  15267  cnco  15305  cnss1  15310  cnss2  15311  cnptopresti  15322  uptx  15358  txrest  15360  psmetres2  15417  xmetres2  15463  xblss2ps  15488  blhalf  15492  blssexps  15513  blssex  15514  blin2  15516  blbas  15517  bdmetval  15584  metcnpi  15599  metcnpi2  15600  qtopbas  15606  tgqioo  15639  cncfss  15667  mulc1cncf  15673  cncfmptid  15681  dedekindicc  15717  ivthdec  15728  cnplimcim  15751  cnplimclemle  15752  cnplimccntop  15754  limccnp2cntop  15761  dvfgg  15772  dvcj  15793  dvrecap  15797  dvmptfsum  15809  dveflem  15810  elply2  15819  ply1termlem  15826  plymullem1  15832  eflt  15859  ptolemy  15908  cos11  15937  rpcxpmul2  15998  cxplt  16001  cxple  16002  cxplt3  16005  apcxp2  16024  rprelogbmul  16040  rprelogbdiv  16042  birthdaylem3  16072  pellexlem3  16076  sgmval  16080  sgmval2  16081  sgmf  16083  sgmmul  16093  perfect  16098  lgsval2lem  16112  lgsdir2lem5  16134  2sqlem6  16222  umgrnloopv  16338  upgredg  16368  usgr1eop  16469  upgredginwlk  16580  wlkv0  16593  clwwlkccatlem  16624  pw1map  17008  pwtrufal  17010  nninfalllem1  17025  nninfsellemqall  17032  nnnninfex  17039  sbthom  17045  qdencn  17046  isomninnlem  17053  trirec0  17067  apdiff  17071  qdiff  17072  iswomninnlem  17073  ismkvnnlem  17076  ltlenmkv  17094