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  10427  elfzodifsumelfzo  10447  ssfzo12bi  10471  rebtwn2z  10515  qbtwnxr  10518  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modqmulmod  10652  modqmulmodr  10653  modqsubdir  10656  frecuzrdgg  10679  nninfinf  10706  seq3val  10723  seqvalcd  10724  seq3feq  10743  seq3f1olemp  10778  seqfeq4g  10794  expp1  10809  expcl2lemap  10814  expnegzap  10836  expadd  10844  expmul  10847  leexp1a  10857  expnlbnd  10927  nn0ltexp2  10972  nn0opth2  10987  bcval  11012  bcval5  11026  bcpasc  11029  hashunsng  11072  seq3coll  11107  iswrdiz  11121  sswrd  11123  ccatalpha  11191  ccatw2s1p1g  11223  swrdwrdsymbg  11246  swrdsb0eq  11247  ccatswrd  11252  pfxf  11264  pfxwrdsymbg  11272  wrd2ind  11305  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12lem3  11314  pfxccatin12  11315  pfxccat3  11316  swrdccat  11317  shftfvalg  11380  shftfval  11383  seq3shft  11400  caucvgrelemrec  11541  resqrexlemdecn  11574  sqrtmul  11597  sqrtdiv  11604  leabs  11636  absexpzap  11642  ltabs  11649  abslt  11650  absle  11651  abssubap0  11652  amgm2  11680  icodiamlt  11742  qdenre  11764  maxleim  11767  maxleastlt  11777  rexico  11783  zmaxcl  11786  minmax  11792  xrmaxleastlt  11818  xrminmax  11827  climuni  11855  cn1lem  11876  iserex  11901  iserle  11904  climserle  11907  climcau  11909  summodclem2a  11944  summodc  11946  isumss  11954  fisumss  11955  fsumadd  11969  isumadd  11994  fsum2dlemstep  11997  fsum2d  11998  fisum0diag2  12010  fsumabs  12028  isumsplit  12054  geolim  12074  geo2lim  12079  geoisum  12080  geoisumr  12081  geoisum1  12082  mertenslemub  12097  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  prodmodclem2  12140  prodmodc  12141  zproddc  12142  fprodseq  12146  fprodcl2lem  12168  fprod2dlemstep  12185  fprodle  12203  fprodmodd  12204  efcvgfsum  12230  eftlcl  12251  reeftlcl  12252  tanaddap  12302  zdvdsdc  12375  dvds2ln  12387  dvdsle  12407  divconjdvds  12412  dvdsext  12418  bitsfzo  12518  gcdsupex  12530  gcdsupcl  12531  bezoutlemmain  12571  bezoutlemaz  12576  bezoutlembi  12578  bezout  12584  gcdmultiplez  12594  dvdsmulgcd  12598  bezoutr  12605  bezoutr1  12606  lcmval  12637  lcmcllem  12641  ncoprmgcdne1b  12663  cncongr1  12677  isprm5  12716  prmdvdsexp  12722  sqrt2irr  12736  pw2dvdslemn  12739  pw2dvdseu  12742  nonsq  12781  powm2modprm  12827  pcmul  12876  pcqmul  12878  pcexp  12884  pcneg  12900  pcdvdstr  12902  pcprmpw2  12908  pcfac  12925  expnprm  12928  prmpwdvds  12930  mul4sq  12969  ssnnctlemct  13069  infpn2  13079  isstruct2r  13095  setsfun  13119  setsfun0  13120  ismndd  13522  submnd0  13529  mhmf1o  13555  resmhm  13572  mhmco  13575  mhmima  13576  dfgrp2  13612  grprcan  13622  grplmulf1o  13659  grplactcnv  13687  pwssub  13698  mhmmnd  13705  mulgval  13711  mulgz  13739  mulgnn0dir  13741  mulgdir  13743  mulgneg2  13745  mhmmulg  13752  issubg4m  13782  nmzsubg  13799  ssnmz  13800  ghmmhmb  13843  resghm  13849  ghmpreima  13855  ghmnsgpreima  13858  ghmf1o  13864  eqgabl  13919  gsumfzconst  13930  rngpropd  13971  srglmhm  14009  srgrmhm  14010  isring  14016  ringadd2  14043  ringpropd  14054  ringlghm  14077  ringrghm  14078  oppr1g  14098  dvdsrex  14115  dvdsrtr  14118  issubrg  14238  unitrrg  14284  islmod  14308  islmodd  14310  lmodfopne  14343  lmodprop2d  14365  lssvacl  14382  lssvsubcl  14383  lssvscl  14392  islss3  14396  lsslss  14398  lss1d  14400  lsspropdg  14448  dflidl2rng  14498  gsumfzfsumlemm  14604  expghmap  14624  mulgghm2  14625  znval  14653  znunit  14676  znrrg  14677  psrbaglesuppg  14689  mplvalcoe  14707  neissex  14892  tgrest  14896  ssrest  14909  restopn2  14910  cnco  14948  cnss1  14953  cnss2  14954  cnptopresti  14965  uptx  15001  txrest  15003  psmetres2  15060  xmetres2  15106  xblss2ps  15131  blhalf  15135  blssexps  15156  blssex  15157  blin2  15159  blbas  15160  bdmetval  15227  metcnpi  15242  metcnpi2  15243  qtopbas  15249  tgqioo  15282  cncfss  15310  mulc1cncf  15316  cncfmptid  15324  dedekindicc  15360  ivthdec  15371  cnplimcim  15394  cnplimclemle  15395  cnplimccntop  15397  limccnp2cntop  15404  dvfgg  15415  dvcj  15436  dvrecap  15440  dvmptfsum  15452  dveflem  15453  elply2  15462  ply1termlem  15469  plymullem1  15475  eflt  15502  ptolemy  15551  cos11  15580  rpcxpmul2  15640  cxplt  15643  cxple  15644  cxplt3  15647  apcxp2  15666  rprelogbmul  15682  rprelogbdiv  15684  sgmval  15710  sgmval2  15711  sgmf  15713  sgmmul  15723  perfect  15728  lgsval2lem  15742  lgsdir2lem5  15764  2sqlem6  15852  umgrnloopv  15968  upgredg  15998  usgr1eop  16099  upgredginwlk  16210  wlkv0  16223  clwwlkccatlem  16254  2omap  16615  pw1map  16617  pwtrufal  16619  nninfalllem1  16631  nninfsellemqall  16638  nnnninfex  16645  sbthom  16651  qdencn  16652  isomninnlem  16655  trirec0  16669  apdiff  16673  iswomninnlem  16674  ismkvnnlem  16677  ltlenmkv  16695