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  1060  simp2ll  1064  simp3ll  1068  rmob  3055  prneimg  3774  exmid01  4198  pwntru  4199  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  poinxp  4695  mpteqb  5606  fvmptt  5607  fcof1  5783  acexmid  5873  dftpos4  6263  tfrlem3ag  6309  tfrlem3a  6310  tfrlemi1  6332  tfrexlem  6334  tfr1onlem3ag  6337  nntr2  6503  dcdifsnid  6504  qsel  6611  ecopovsymg  6633  ecopoverg  6635  th3qlem1  6636  mapss  6690  xpmapenlem  6848  findcard2  6888  findcard2s  6889  findcard2sd  6891  unfiin  6924  f1finf1o  6945  fidcenumlemrk  6952  fidcenumlemr  6953  fidcenum  6954  sbthlemi6  6960  sbthlemi8  6962  elfi2  6970  supisolem  7006  enumct  7113  ismkvnex  7152  exmidontriimlem4  7222  netap  7252  2omotaplemap  7255  cc2lem  7264  dfplpq2  7352  dfmpq2  7353  mulpipqqs  7371  distrnqg  7385  ltexnqq  7406  subhalfnqq  7412  prarloclemarch  7416  nnnq0lem1  7444  distrnq0  7457  npsspw  7469  prarloclemlo  7492  prarloclem3  7495  prarloclemcalc  7500  genplt2i  7508  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  ltprordil  7587  ltexprlemlol  7600  ltexprlemupu  7602  addextpr  7619  recexprlemopl  7623  recexprlemdisj  7628  recexprlem1ssl  7631  aptiprleml  7637  prsrlem1  7740  recexgt0sr  7771  addcnsr  7832  mulcnsr  7833  mulcnsrec  7841  axaddcl  7862  axmulcl  7864  axmulcom  7869  rereceu  7887  ltntri  8083  cnegexlem1  8130  cnegex  8133  addsub4  8198  le2add  8399  lt2add  8400  lt2sub  8415  le2sub  8416  rereim  8541  apreim  8558  mulreim  8559  addext  8565  mulext  8569  receuap  8624  rec11ap  8665  rec11rap  8666  divdivdivap  8668  ddcanap  8681  divadddivap  8682  divsubdivap  8683  conjmulap  8684  rerecclap  8685  subrecap  8794  recgt0  8805  prodgt0gt0  8806  prodgt0  8807  prodge0  8809  ltmul12a  8815  lemul12a  8817  lemulge11  8821  lt2mul2div  8834  ltrec  8838  lerec  8839  lt2msq  8841  ltrec1  8843  le2msq  8856  msq11  8857  ledivp1  8858  mulle0r  8899  peano5uzti  9359  eluzuzle  9534  qreccl  9640  elpq  9646  xrltso  9794  z2ge  9824  xpncan  9869  xaddge0  9876  xle2add  9877  xleaddadd  9885  ixxss1  9902  ixxss2  9903  elioc2  9934  divelunit  10000  fzass4  10059  fzrev  10081  fzonmapblen  10184  elfzodifsumelfzo  10198  ssfzo12bi  10222  rebtwn2z  10252  qbtwnxr  10255  modqid  10346  modqcyc  10356  modqaddabs  10359  modqaddmod  10360  mulqaddmodid  10361  modqadd2mod  10371  modqltm1p1mod  10373  modqsubmod  10379  modqsubmodmod  10380  modqmulmod  10386  modqmulmodr  10387  modqsubdir  10390  frecuzrdgg  10413  seq3val  10455  seqvalcd  10456  seq3feq  10469  seq3f1olemp  10499  expp1  10524  expcl2lemap  10529  expnegzap  10551  expadd  10559  expmul  10562  leexp1a  10572  expnlbnd  10641  nn0ltexp2  10685  nn0opth2  10699  bcval  10724  bcval5  10738  bcpasc  10741  hashunsng  10782  seq3coll  10817  shftfvalg  10822  shftfval  10825  seq3shft  10842  caucvgrelemrec  10983  resqrexlemdecn  11016  sqrtmul  11039  sqrtdiv  11046  leabs  11078  absexpzap  11084  ltabs  11091  abslt  11092  absle  11093  abssubap0  11094  amgm2  11122  icodiamlt  11184  qdenre  11206  maxleim  11209  maxleastlt  11219  rexico  11225  zmaxcl  11228  minmax  11233  xrmaxleastlt  11259  xrminmax  11268  climuni  11296  cn1lem  11317  iserex  11342  iserle  11345  climserle  11348  climcau  11350  summodclem2a  11384  summodc  11386  isumss  11394  fisumss  11395  fsumadd  11409  isumadd  11434  fsum2dlemstep  11437  fsum2d  11438  fisum0diag2  11450  fsumabs  11468  isumsplit  11494  geolim  11514  geo2lim  11519  geoisum  11520  geoisumr  11521  geoisum1  11522  mertenslemub  11537  mertenslemi1  11538  mertenslem2  11539  mertensabs  11540  prodmodclem2  11580  prodmodc  11581  zproddc  11582  fprodseq  11586  fprodcl2lem  11608  fprod2dlemstep  11625  fprodle  11643  fprodmodd  11644  efcvgfsum  11670  eftlcl  11691  reeftlcl  11692  tanaddap  11742  zdvdsdc  11814  dvds2ln  11826  dvdsle  11844  divconjdvds  11849  dvdsext  11855  gcdsupex  11952  gcdsupcl  11953  bezoutlemmain  11993  bezoutlemaz  11998  bezoutlembi  12000  bezout  12006  gcdmultiplez  12016  dvdsmulgcd  12020  bezoutr  12027  bezoutr1  12028  lcmval  12057  lcmcllem  12061  ncoprmgcdne1b  12083  cncongr1  12097  isprm5  12136  prmdvdsexp  12142  sqrt2irr  12156  pw2dvdslemn  12159  pw2dvdseu  12162  nonsq  12201  powm2modprm  12246  pcmul  12295  pcqmul  12297  pcexp  12303  pcneg  12318  pcdvdstr  12320  pcprmpw2  12326  pcfac  12342  expnprm  12345  prmpwdvds  12347  mul4sq  12386  ssnnctlemct  12441  infpn2  12451  isstruct2r  12467  setsfun  12491  setsfun0  12492  ismndd  12832  submnd0  12839  mhmf1o  12855  mhmco  12868  mhmima  12869  dfgrp2  12896  grprcan  12904  grplmulf1o  12938  grplactcnv  12966  mhmmnd  12974  mulgval  12980  mulgz  13004  mulgnn0dir  13006  mulgdir  13008  mulgneg2  13010  mhmmulg  13017  issubg4m  13046  nmzsubg  13063  ssnmz  13064  srglmhm  13169  srgrmhm  13170  isring  13176  ringadd2  13203  ringpropd  13210  oppr1g  13245  dvdsrex  13260  dvdsrtr  13263  issubrg  13342  neissex  13596  tgrest  13600  ssrest  13613  restopn2  13614  cnco  13652  cnss1  13657  cnss2  13658  cnptopresti  13669  uptx  13705  txrest  13707  psmetres2  13764  xmetres2  13810  xblss2ps  13835  blhalf  13839  blssexps  13860  blssex  13861  blin2  13863  blbas  13864  bdmetval  13931  metcnpi  13946  metcnpi2  13947  qtopbas  13953  tgqioo  13978  cncfss  14001  mulc1cncf  14007  cncfmptid  14014  dedekindicc  14042  ivthdec  14053  cnplimcim  14067  cnplimclemle  14068  cnplimccntop  14070  limccnp2cntop  14077  dvfgg  14088  dvcj  14104  dvrecap  14108  dveflem  14118  eflt  14127  ptolemy  14176  cos11  14205  cxplt  14267  cxple  14268  cxplt3  14271  apcxp2  14289  rprelogbmul  14304  rprelogbdiv  14306  lgsval2lem  14342  lgsdir2lem5  14364  2sqlem6  14387  pwtrufal  14667  nninfalllem1  14677  nninfsellemqall  14684  sbthom  14694  qdencn  14695  isomninnlem  14698  trirec0  14712  apdiff  14716  iswomninnlem  14717  ismkvnnlem  14720  ltlenmkv  14737