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  3029  prneimg  3737  exmid01  4159  pwntru  4160  ordtri2or2exmidlem  4485  onsucelsucexmidlem  4488  poinxp  4655  mpteqb  5558  fvmptt  5559  fcof1  5733  acexmid  5823  grprinvlem  6015  dftpos4  6210  tfrlem3ag  6256  tfrlem3a  6257  tfrlemi1  6279  tfrexlem  6281  tfr1onlem3ag  6284  nntr2  6450  dcdifsnid  6451  qsel  6557  ecopovsymg  6579  ecopoverg  6581  th3qlem1  6582  mapss  6636  xpmapenlem  6794  findcard2  6834  findcard2s  6835  findcard2sd  6837  unfiin  6870  f1finf1o  6891  fidcenumlemrk  6898  fidcenumlemr  6899  fidcenum  6900  sbthlemi6  6906  sbthlemi8  6908  elfi2  6916  supisolem  6952  enumct  7059  ismkvnex  7098  exmidontriimlem4  7159  cc2lem  7186  dfplpq2  7274  dfmpq2  7275  mulpipqqs  7293  distrnqg  7307  ltexnqq  7328  subhalfnqq  7334  prarloclemarch  7338  nnnq0lem1  7366  distrnq0  7379  npsspw  7391  prarloclemlo  7414  prarloclem3  7417  prarloclemcalc  7422  genplt2i  7430  distrlem1prl  7502  distrlem1pru  7503  distrlem4prl  7504  distrlem4pru  7505  ltprordil  7509  ltexprlemlol  7522  ltexprlemupu  7524  addextpr  7541  recexprlemopl  7545  recexprlemdisj  7550  recexprlem1ssl  7553  aptiprleml  7559  prsrlem1  7662  recexgt0sr  7693  addcnsr  7754  mulcnsr  7755  mulcnsrec  7763  axaddcl  7784  axmulcl  7786  axmulcom  7791  rereceu  7809  ltntri  8003  cnegexlem1  8050  cnegex  8053  addsub4  8118  le2add  8319  lt2add  8320  lt2sub  8335  le2sub  8336  rereim  8461  apreim  8478  mulreim  8479  addext  8485  mulext  8489  receuap  8543  rec11ap  8583  rec11rap  8584  divdivdivap  8586  ddcanap  8599  divadddivap  8600  divsubdivap  8601  conjmulap  8602  rerecclap  8603  subrecap  8711  recgt0  8721  prodgt0gt0  8722  prodgt0  8723  prodge0  8725  ltmul12a  8731  lemul12a  8733  lemulge11  8737  lt2mul2div  8750  ltrec  8754  lerec  8755  lt2msq  8757  ltrec1  8759  le2msq  8772  msq11  8773  ledivp1  8774  mulle0r  8815  peano5uzti  9272  eluzuzle  9447  qreccl  9551  elpq  9557  xrltso  9703  z2ge  9730  xpncan  9775  xaddge0  9782  xle2add  9783  xleaddadd  9791  ixxss1  9808  ixxss2  9809  elioc2  9840  divelunit  9906  fzass4  9964  fzrev  9986  fzonmapblen  10086  elfzodifsumelfzo  10100  ssfzo12bi  10124  rebtwn2z  10154  qbtwnxr  10157  modqid  10248  modqcyc  10258  modqaddabs  10261  modqaddmod  10262  mulqaddmodid  10263  modqadd2mod  10273  modqltm1p1mod  10275  modqsubmod  10281  modqsubmodmod  10282  modqmulmod  10288  modqmulmodr  10289  modqsubdir  10292  frecuzrdgg  10315  seq3val  10357  seqvalcd  10358  seq3feq  10371  seq3f1olemp  10401  expp1  10426  expcl2lemap  10431  expnegzap  10453  expadd  10461  expmul  10464  leexp1a  10474  expnlbnd  10542  nn0opth2  10598  bcval  10623  bcval5  10637  bcpasc  10640  hashunsng  10681  seq3coll  10713  shftfvalg  10718  shftfval  10721  seq3shft  10738  caucvgrelemrec  10879  resqrexlemdecn  10912  sqrtmul  10935  sqrtdiv  10942  leabs  10974  absexpzap  10980  ltabs  10987  abslt  10988  absle  10989  abssubap0  10990  amgm2  11018  icodiamlt  11080  qdenre  11102  maxleim  11105  maxleastlt  11115  rexico  11121  zmaxcl  11124  minmax  11129  xrmaxleastlt  11153  xrminmax  11162  climuni  11190  cn1lem  11211  iserex  11236  iserle  11239  climserle  11242  climcau  11244  summodclem2a  11278  summodc  11280  isumss  11288  fisumss  11289  fsumadd  11303  isumadd  11328  fsum2dlemstep  11331  fsum2d  11332  fisum0diag2  11344  fsumabs  11362  isumsplit  11388  geolim  11408  geo2lim  11413  geoisum  11414  geoisumr  11415  geoisum1  11416  mertenslemub  11431  mertenslemi1  11432  mertenslem2  11433  mertensabs  11434  prodmodclem2  11474  prodmodc  11475  zproddc  11476  fprodseq  11480  fprodcl2lem  11502  fprod2dlemstep  11519  fprodle  11537  fprodmodd  11538  efcvgfsum  11564  eftlcl  11585  reeftlcl  11586  tanaddap  11636  zdvdsdc  11708  dvds2ln  11720  dvdsle  11736  divconjdvds  11741  dvdsext  11747  gcdsupex  11841  gcdsupcl  11842  bezoutlemmain  11882  bezoutlemaz  11887  bezoutlembi  11889  bezout  11895  gcdmultiplez  11905  dvdsmulgcd  11909  bezoutr  11916  bezoutr1  11917  lcmval  11940  lcmcllem  11944  ncoprmgcdne1b  11966  cncongr1  11980  prmdvdsexp  12023  sqrt2irr  12037  pw2dvdslemn  12040  pw2dvdseu  12043  nonsq  12082  powm2modprm  12127  ssnnctlemct  12186  isstruct2r  12212  setsfun  12236  setsfun0  12237  neissex  12576  tgrest  12580  ssrest  12593  restopn2  12594  cnco  12632  cnss1  12637  cnss2  12638  cnptopresti  12649  uptx  12685  txrest  12687  psmetres2  12744  xmetres2  12790  xblss2ps  12815  blhalf  12819  blssexps  12840  blssex  12841  blin2  12843  blbas  12844  bdmetval  12911  metcnpi  12926  metcnpi2  12927  qtopbas  12933  tgqioo  12958  cncfss  12981  mulc1cncf  12987  cncfmptid  12994  dedekindicc  13022  ivthdec  13033  cnplimcim  13047  cnplimclemle  13048  cnplimccntop  13050  limccnp2cntop  13057  dvfgg  13068  dvcj  13084  dvrecap  13088  dveflem  13098  eflt  13107  ptolemy  13156  cos11  13185  cxplt  13247  cxple  13248  cxplt3  13251  apcxp2  13269  rprelogbmul  13283  rprelogbdiv  13285  pwtrufal  13580  nninfalllem1  13591  nninfsellemqall  13598  sbthom  13608  qdencn  13609  isomninnlem  13612  trirec0  13626  apdiff  13630  iswomninnlem  13631  ismkvnnlem  13634