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  1050  simp2ll  1054  simp3ll  1058  rmob  3042  prneimg  3753  exmid01  4176  pwntru  4177  ordtri2or2exmidlem  4502  onsucelsucexmidlem  4505  poinxp  4672  mpteqb  5575  fvmptt  5576  fcof1  5750  acexmid  5840  grprinvlem  6032  dftpos4  6227  tfrlem3ag  6273  tfrlem3a  6274  tfrlemi1  6296  tfrexlem  6298  tfr1onlem3ag  6301  nntr2  6467  dcdifsnid  6468  qsel  6574  ecopovsymg  6596  ecopoverg  6598  th3qlem1  6599  mapss  6653  xpmapenlem  6811  findcard2  6851  findcard2s  6852  findcard2sd  6854  unfiin  6887  f1finf1o  6908  fidcenumlemrk  6915  fidcenumlemr  6916  fidcenum  6917  sbthlemi6  6923  sbthlemi8  6925  elfi2  6933  supisolem  6969  enumct  7076  ismkvnex  7115  exmidontriimlem4  7176  cc2lem  7203  dfplpq2  7291  dfmpq2  7292  mulpipqqs  7310  distrnqg  7324  ltexnqq  7345  subhalfnqq  7351  prarloclemarch  7355  nnnq0lem1  7383  distrnq0  7396  npsspw  7408  prarloclemlo  7431  prarloclem3  7434  prarloclemcalc  7439  genplt2i  7447  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  ltprordil  7526  ltexprlemlol  7539  ltexprlemupu  7541  addextpr  7558  recexprlemopl  7562  recexprlemdisj  7567  recexprlem1ssl  7570  aptiprleml  7576  prsrlem1  7679  recexgt0sr  7710  addcnsr  7771  mulcnsr  7772  mulcnsrec  7780  axaddcl  7801  axmulcl  7803  axmulcom  7808  rereceu  7826  ltntri  8022  cnegexlem1  8069  cnegex  8072  addsub4  8137  le2add  8338  lt2add  8339  lt2sub  8354  le2sub  8355  rereim  8480  apreim  8497  mulreim  8498  addext  8504  mulext  8508  receuap  8562  rec11ap  8602  rec11rap  8603  divdivdivap  8605  ddcanap  8618  divadddivap  8619  divsubdivap  8620  conjmulap  8621  rerecclap  8622  subrecap  8731  recgt0  8741  prodgt0gt0  8742  prodgt0  8743  prodge0  8745  ltmul12a  8751  lemul12a  8753  lemulge11  8757  lt2mul2div  8770  ltrec  8774  lerec  8775  lt2msq  8777  ltrec1  8779  le2msq  8792  msq11  8793  ledivp1  8794  mulle0r  8835  peano5uzti  9295  eluzuzle  9470  qreccl  9576  elpq  9582  xrltso  9728  z2ge  9758  xpncan  9803  xaddge0  9810  xle2add  9811  xleaddadd  9819  ixxss1  9836  ixxss2  9837  elioc2  9868  divelunit  9934  fzass4  9993  fzrev  10015  fzonmapblen  10118  elfzodifsumelfzo  10132  ssfzo12bi  10156  rebtwn2z  10186  qbtwnxr  10189  modqid  10280  modqcyc  10290  modqaddabs  10293  modqaddmod  10294  mulqaddmodid  10295  modqadd2mod  10305  modqltm1p1mod  10307  modqsubmod  10313  modqsubmodmod  10314  modqmulmod  10320  modqmulmodr  10321  modqsubdir  10324  frecuzrdgg  10347  seq3val  10389  seqvalcd  10390  seq3feq  10403  seq3f1olemp  10433  expp1  10458  expcl2lemap  10463  expnegzap  10485  expadd  10493  expmul  10496  leexp1a  10506  expnlbnd  10575  nn0ltexp2  10619  nn0opth2  10633  bcval  10658  bcval5  10672  bcpasc  10675  hashunsng  10716  seq3coll  10751  shftfvalg  10756  shftfval  10759  seq3shft  10776  caucvgrelemrec  10917  resqrexlemdecn  10950  sqrtmul  10973  sqrtdiv  10980  leabs  11012  absexpzap  11018  ltabs  11025  abslt  11026  absle  11027  abssubap0  11028  amgm2  11056  icodiamlt  11118  qdenre  11140  maxleim  11143  maxleastlt  11153  rexico  11159  zmaxcl  11162  minmax  11167  xrmaxleastlt  11193  xrminmax  11202  climuni  11230  cn1lem  11251  iserex  11276  iserle  11279  climserle  11282  climcau  11284  summodclem2a  11318  summodc  11320  isumss  11328  fisumss  11329  fsumadd  11343  isumadd  11368  fsum2dlemstep  11371  fsum2d  11372  fisum0diag2  11384  fsumabs  11402  isumsplit  11428  geolim  11448  geo2lim  11453  geoisum  11454  geoisumr  11455  geoisum1  11456  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodcl2lem  11542  fprod2dlemstep  11559  fprodle  11577  fprodmodd  11578  efcvgfsum  11604  eftlcl  11625  reeftlcl  11626  tanaddap  11676  zdvdsdc  11748  dvds2ln  11760  dvdsle  11778  divconjdvds  11783  dvdsext  11789  gcdsupex  11886  gcdsupcl  11887  bezoutlemmain  11927  bezoutlemaz  11932  bezoutlembi  11934  bezout  11940  gcdmultiplez  11950  dvdsmulgcd  11954  bezoutr  11961  bezoutr1  11962  lcmval  11991  lcmcllem  11995  ncoprmgcdne1b  12017  cncongr1  12031  isprm5  12070  prmdvdsexp  12076  sqrt2irr  12090  pw2dvdslemn  12093  pw2dvdseu  12096  nonsq  12135  powm2modprm  12180  pcmul  12229  pcqmul  12231  pcexp  12237  pcneg  12252  pcdvdstr  12254  pcprmpw2  12260  pcfac  12276  expnprm  12279  prmpwdvds  12281  mul4sq  12320  ssnnctlemct  12375  infpn2  12385  isstruct2r  12401  setsfun  12425  setsfun0  12426  neissex  12765  tgrest  12769  ssrest  12782  restopn2  12783  cnco  12821  cnss1  12826  cnss2  12827  cnptopresti  12838  uptx  12874  txrest  12876  psmetres2  12933  xmetres2  12979  xblss2ps  13004  blhalf  13008  blssexps  13029  blssex  13030  blin2  13032  blbas  13033  bdmetval  13100  metcnpi  13115  metcnpi2  13116  qtopbas  13122  tgqioo  13147  cncfss  13170  mulc1cncf  13176  cncfmptid  13183  dedekindicc  13211  ivthdec  13222  cnplimcim  13236  cnplimclemle  13237  cnplimccntop  13239  limccnp2cntop  13246  dvfgg  13257  dvcj  13273  dvrecap  13277  dveflem  13287  eflt  13296  ptolemy  13345  cos11  13374  cxplt  13436  cxple  13437  cxplt3  13440  apcxp2  13458  rprelogbmul  13473  rprelogbdiv  13475  lgsval2lem  13511  lgsdir2lem5  13533  2sqlem6  13556  pwtrufal  13837  nninfalllem1  13848  nninfsellemqall  13855  sbthom  13865  qdencn  13866  isomninnlem  13869  trirec0  13883  apdiff  13887  iswomninnlem  13888  ismkvnnlem  13891