Theorem simpll 519

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp1ll  1045  simp2ll  1049  simp3ll  1053  rmob  3005  prneimg  3709  exmid01  4129  pwntru  4130  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  poinxp  4616  mpteqb  5519  fvmptt  5520  fcof1  5692  acexmid  5781  grprinvlem  5973  dftpos4  6168  tfrlem3ag  6214  tfrlem3a  6215  tfrlemi1  6237  tfrexlem  6239  tfr1onlem3ag  6242  nntr2  6407  dcdifsnid  6408  qsel  6514  ecopovsymg  6536  ecopoverg  6538  th3qlem1  6539  mapss  6593  xpmapenlem  6751  findcard2  6791  findcard2s  6792  findcard2sd  6794  unfiin  6822  f1finf1o  6843  fidcenumlemrk  6850  fidcenumlemr  6851  fidcenum  6852  sbthlemi6  6858  sbthlemi8  6860  elfi2  6868  supisolem  6903  enumct  7008  ismkvnex  7037  cc2lem  7098  dfplpq2  7186  dfmpq2  7187  mulpipqqs  7205  distrnqg  7219  ltexnqq  7240  subhalfnqq  7246  prarloclemarch  7250  nnnq0lem1  7278  distrnq0  7291  npsspw  7303  prarloclemlo  7326  prarloclem3  7329  prarloclemcalc  7334  genplt2i  7342  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  ltprordil  7421  ltexprlemlol  7434  ltexprlemupu  7436  addextpr  7453  recexprlemopl  7457  recexprlemdisj  7462  recexprlem1ssl  7465  aptiprleml  7471  prsrlem1  7574  recexgt0sr  7605  addcnsr  7666  mulcnsr  7667  mulcnsrec  7675  axaddcl  7696  axmulcl  7698  axmulcom  7703  rereceu  7721  ltntri  7914  cnegexlem1  7961  cnegex  7964  addsub4  8029  le2add  8230  lt2add  8231  lt2sub  8246  le2sub  8247  rereim  8372  apreim  8389  mulreim  8390  addext  8396  mulext  8400  receuap  8454  rec11ap  8494  rec11rap  8495  divdivdivap  8497  ddcanap  8510  divadddivap  8511  divsubdivap  8512  conjmulap  8513  rerecclap  8514  subrecap  8622  recgt0  8632  prodgt0gt0  8633  prodgt0  8634  prodge0  8636  ltmul12a  8642  lemul12a  8644  lemulge11  8648  lt2mul2div  8661  ltrec  8665  lerec  8666  lt2msq  8668  ltrec1  8670  le2msq  8683  msq11  8684  ledivp1  8685  mulle0r  8726  peano5uzti  9183  eluzuzle  9358  qreccl  9461  elpq  9467  xrltso  9612  z2ge  9639  xpncan  9684  xaddge0  9691  xle2add  9692  xleaddadd  9700  ixxss1  9717  ixxss2  9718  elioc2  9749  divelunit  9815  fzass4  9873  fzrev  9895  fzonmapblen  9995  elfzodifsumelfzo  10009  ssfzo12bi  10033  rebtwn2z  10063  qbtwnxr  10066  modqid  10153  modqcyc  10163  modqaddabs  10166  modqaddmod  10167  mulqaddmodid  10168  modqadd2mod  10178  modqltm1p1mod  10180  modqsubmod  10186  modqsubmodmod  10187  modqmulmod  10193  modqmulmodr  10194  modqsubdir  10197  frecuzrdgg  10220  seq3val  10262  seqvalcd  10263  seq3feq  10276  seq3f1olemp  10306  expp1  10331  expcl2lemap  10336  expnegzap  10358  expadd  10366  expmul  10369  leexp1a  10379  expnlbnd  10447  nn0opth2  10502  bcval  10527  bcval5  10541  bcpasc  10544  hashunsng  10585  seq3coll  10617  shftfvalg  10622  shftfval  10625  seq3shft  10642  caucvgrelemrec  10783  resqrexlemdecn  10816  sqrtmul  10839  sqrtdiv  10846  leabs  10878  absexpzap  10884  ltabs  10891  abslt  10892  absle  10893  abssubap0  10894  amgm2  10922  icodiamlt  10984  qdenre  11006  maxleim  11009  maxleastlt  11019  rexico  11025  zmaxcl  11028  minmax  11033  xrmaxleastlt  11057  xrminmax  11066  climuni  11094  cn1lem  11115  iserex  11140  iserle  11143  climserle  11146  climcau  11148  summodclem2a  11182  summodc  11184  isumss  11192  fisumss  11193  fsumadd  11207  isumadd  11232  fsum2dlemstep  11235  fsum2d  11236  fisum0diag2  11248  fsumabs  11266  isumsplit  11292  geolim  11312  geo2lim  11317  geoisum  11318  geoisumr  11319  geoisum1  11320  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  efcvgfsum  11410  eftlcl  11431  reeftlcl  11432  tanaddap  11482  zdvdsdc  11550  dvds2ln  11562  dvdsle  11578  divconjdvds  11583  dvdsext  11589  gcdsupex  11682  gcdsupcl  11683  bezoutlemmain  11722  bezoutlemaz  11727  bezoutlembi  11729  bezout  11735  gcdmultiplez  11745  dvdsmulgcd  11749  bezoutr  11756  bezoutr1  11757  lcmval  11780  lcmcllem  11784  ncoprmgcdne1b  11806  cncongr1  11820  prmdvdsexp  11862  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseu  11882  nonsq  11921  isstruct2r  12009  setsfun  12033  setsfun0  12034  neissex  12373  tgrest  12377  ssrest  12390  restopn2  12391  cnco  12429  cnss1  12434  cnss2  12435  cnptopresti  12446  uptx  12482  txrest  12484  psmetres2  12541  xmetres2  12587  xblss2ps  12612  blhalf  12616  blssexps  12637  blssex  12638  blin2  12640  blbas  12641  bdmetval  12708  metcnpi  12723  metcnpi2  12724  qtopbas  12730  tgqioo  12755  cncfss  12778  mulc1cncf  12784  cncfmptid  12791  dedekindicc  12819  ivthdec  12830  cnplimcim  12844  cnplimclemle  12845  cnplimccntop  12847  limccnp2cntop  12854  dvfgg  12865  dvcj  12881  dvrecap  12885  dveflem  12895  eflt  12904  ptolemy  12953  cos11  12982  cxplt  13044  cxple  13045  cxplt3  13048  apcxp2  13066  rprelogbmul  13080  rprelogbdiv  13082  pwtrufal  13365  nninfalllem1  13378  nninfsellemqall  13386  sbthom  13396  qdencn  13397  isomninnlem  13400  trirec0  13412  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419