Theorem simpll 527

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 488	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  1086  simp2ll  1090  simp3ll  1094  rmob  3125  ifnefals  3650  prneimg  3857  exmid01  4288  pwntru  4289  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  poinxp  4795  mpteqb  5737  fvmptt  5738  fcof1  5924  acexmid  6017  dftpos4  6429  tfrlem3ag  6475  tfrlem3a  6476  tfrlemi1  6498  tfrexlem  6500  tfr1onlem3ag  6503  nntr2  6671  dcdifsnid  6672  qsel  6781  ecopovsymg  6803  ecopoverg  6805  th3qlem1  6806  mapss  6860  xpmapenlem  7035  findcard2  7078  findcard2s  7079  findcard2sd  7081  unfiin  7118  f1finf1o  7146  fidcenumlemrk  7153  fidcenumlemr  7154  fidcenum  7155  sbthlemi6  7161  sbthlemi8  7163  elfi2  7171  supisolem  7207  enumct  7314  nninfninc  7322  ismkvnex  7354  exmidontriimlem4  7439  netap  7473  2omotaplemap  7476  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  ltexnqq  7628  subhalfnqq  7634  prarloclemarch  7638  nnnq0lem1  7666  distrnq0  7679  npsspw  7691  prarloclemlo  7714  prarloclem3  7717  prarloclemcalc  7722  genplt2i  7730  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemlol  7822  ltexprlemupu  7824  addextpr  7841  recexprlemopl  7845  recexprlemdisj  7850  recexprlem1ssl  7853  aptiprleml  7859  prsrlem1  7962  recexgt0sr  7993  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axaddcl  8084  axmulcl  8086  axmulcom  8091  rereceu  8109  mpomulf  8169  ltntri  8307  cnegexlem1  8354  cnegex  8357  addsub4  8422  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  rereim  8766  apreim  8783  mulreim  8784  addext  8790  mulext  8794  receuap  8849  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  divsubdivap  8908  conjmulap  8909  rerecclap  8910  subrecap  9019  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  ltmul12a  9040  lemul12a  9042  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lt2msq  9066  ltrec1  9068  le2msq  9081  msq11  9082  ledivp1  9083  mulle0r  9124  peano5uzti  9588  eluzuzle  9764  qreccl  9876  elpq  9883  xrltso  10031  z2ge  10061  xpncan  10106  xaddge0  10113  xle2add  10114  xleaddadd  10122  ixxss1  10139  ixxss2  10140  elioc2  10171  divelunit  10237  fzass4  10297  fzrev  10319  fzonmapblen  10426  elfzodifsumelfzo  10446  ssfzo12bi  10470  rebtwn2z  10514  qbtwnxr  10517  modqid  10611  modqcyc  10621  modqaddabs  10624  modqaddmod  10625  mulqaddmodid  10626  modqadd2mod  10636  modqltm1p1mod  10638  modqsubmod  10644  modqsubmodmod  10645  modqmulmod  10651  modqmulmodr  10652  modqsubdir  10655  frecuzrdgg  10678  nninfinf  10705  seq3val  10722  seqvalcd  10723  seq3feq  10742  seq3f1olemp  10777  seqfeq4g  10793  expp1  10808  expcl2lemap  10813  expnegzap  10835  expadd  10843  expmul  10846  leexp1a  10856  expnlbnd  10926  nn0ltexp2  10971  nn0opth2  10986  bcval  11011  bcval5  11025  bcpasc  11028  hashunsng  11071  seq3coll  11106  iswrdiz  11120  sswrd  11122  ccatalpha  11190  ccatw2s1p1g  11222  swrdwrdsymbg  11245  swrdsb0eq  11246  ccatswrd  11251  pfxf  11263  pfxwrdsymbg  11271  wrd2ind  11304  swrdccatin2  11310  pfxccatin12lem2  11312  pfxccatin12lem3  11313  pfxccatin12  11314  pfxccat3  11315  swrdccat  11316  shftfvalg  11379  shftfval  11382  seq3shft  11399  caucvgrelemrec  11540  resqrexlemdecn  11573  sqrtmul  11596  sqrtdiv  11603  leabs  11635  absexpzap  11641  ltabs  11648  abslt  11649  absle  11650  abssubap0  11651  amgm2  11679  icodiamlt  11741  qdenre  11763  maxleim  11766  maxleastlt  11776  rexico  11782  zmaxcl  11785  minmax  11791  xrmaxleastlt  11817  xrminmax  11826  climuni  11854  cn1lem  11875  iserex  11900  iserle  11903  climserle  11906  climcau  11908  summodclem2a  11943  summodc  11945  isumss  11953  fisumss  11954  fsumadd  11968  isumadd  11993  fsum2dlemstep  11996  fsum2d  11997  fisum0diag2  12009  fsumabs  12027  isumsplit  12053  geolim  12073  geo2lim  12078  geoisum  12079  geoisumr  12080  geoisum1  12081  mertenslemub  12096  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  prodmodclem2  12139  prodmodc  12140  zproddc  12141  fprodseq  12145  fprodcl2lem  12167  fprod2dlemstep  12184  fprodle  12202  fprodmodd  12203  efcvgfsum  12229  eftlcl  12250  reeftlcl  12251  tanaddap  12301  zdvdsdc  12374  dvds2ln  12386  dvdsle  12406  divconjdvds  12411  dvdsext  12417  bitsfzo  12517  gcdsupex  12529  gcdsupcl  12530  bezoutlemmain  12570  bezoutlemaz  12575  bezoutlembi  12577  bezout  12583  gcdmultiplez  12593  dvdsmulgcd  12597  bezoutr  12604  bezoutr1  12605  lcmval  12636  lcmcllem  12640  ncoprmgcdne1b  12662  cncongr1  12676  isprm5  12715  prmdvdsexp  12721  sqrt2irr  12735  pw2dvdslemn  12738  pw2dvdseu  12741  nonsq  12780  powm2modprm  12826  pcmul  12875  pcqmul  12877  pcexp  12883  pcneg  12899  pcdvdstr  12901  pcprmpw2  12907  pcfac  12924  expnprm  12927  prmpwdvds  12929  mul4sq  12968  ssnnctlemct  13068  infpn2  13078  isstruct2r  13094  setsfun  13118  setsfun0  13119  ismndd  13521  submnd0  13528  mhmf1o  13554  resmhm  13571  mhmco  13574  mhmima  13575  dfgrp2  13611  grprcan  13621  grplmulf1o  13658  grplactcnv  13686  pwssub  13697  mhmmnd  13704  mulgval  13710  mulgz  13738  mulgnn0dir  13740  mulgdir  13742  mulgneg2  13744  mhmmulg  13751  issubg4m  13781  nmzsubg  13798  ssnmz  13799  ghmmhmb  13842  resghm  13848  ghmpreima  13854  ghmnsgpreima  13857  ghmf1o  13863  eqgabl  13918  gsumfzconst  13929  rngpropd  13970  srglmhm  14008  srgrmhm  14009  isring  14015  ringadd2  14042  ringpropd  14053  ringlghm  14076  ringrghm  14077  oppr1g  14097  dvdsrex  14114  dvdsrtr  14117  issubrg  14237  unitrrg  14283  islmod  14307  islmodd  14309  lmodfopne  14342  lmodprop2d  14364  lssvacl  14381  lssvsubcl  14382  lssvscl  14391  islss3  14395  lsslss  14397  lss1d  14399  lsspropdg  14447  dflidl2rng  14497  gsumfzfsumlemm  14603  expghmap  14623  mulgghm2  14624  znval  14652  znunit  14675  znrrg  14676  psrbaglesuppg  14688  mplvalcoe  14706  neissex  14891  tgrest  14895  ssrest  14908  restopn2  14909  cnco  14947  cnss1  14952  cnss2  14953  cnptopresti  14964  uptx  15000  txrest  15002  psmetres2  15059  xmetres2  15105  xblss2ps  15130  blhalf  15134  blssexps  15155  blssex  15156  blin2  15158  blbas  15159  bdmetval  15226  metcnpi  15241  metcnpi2  15242  qtopbas  15248  tgqioo  15281  cncfss  15309  mulc1cncf  15315  cncfmptid  15323  dedekindicc  15359  ivthdec  15370  cnplimcim  15393  cnplimclemle  15394  cnplimccntop  15396  limccnp2cntop  15403  dvfgg  15414  dvcj  15435  dvrecap  15439  dvmptfsum  15451  dveflem  15452  elply2  15461  ply1termlem  15468  plymullem1  15474  eflt  15501  ptolemy  15550  cos11  15579  rpcxpmul2  15639  cxplt  15642  cxple  15643  cxplt3  15646  apcxp2  15665  rprelogbmul  15681  rprelogbdiv  15683  sgmval  15709  sgmval2  15710  sgmf  15712  sgmmul  15722  perfect  15727  lgsval2lem  15741  lgsdir2lem5  15763  2sqlem6  15851  umgrnloopv  15967  upgredg  15997  usgr1eop  16098  upgredginwlk  16209  wlkv0  16222  clwwlkccatlem  16253  2omap  16597  pw1map  16599  pwtrufal  16601  nninfalllem1  16613  nninfsellemqall  16620  nnnninfex  16627  sbthom  16633  qdencn  16634  isomninnlem  16637  trirec0  16651  apdiff  16655  iswomninnlem  16656  ismkvnnlem  16659  ltlenmkv  16677