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  3124  ifnefals  3651  prneimg  3858  exmid01  4290  pwntru  4291  ordtri2or2exmidlem  4626  onsucelsucexmidlem  4629  poinxp  4797  mpteqb  5740  fvmptt  5741  fcof1  5929  acexmid  6022  dftpos4  6434  tfrlem3ag  6480  tfrlem3a  6481  tfrlemi1  6503  tfrexlem  6505  tfr1onlem3ag  6508  nntr2  6676  dcdifsnid  6677  qsel  6786  ecopovsymg  6808  ecopoverg  6810  th3qlem1  6811  mapss  6865  xpmapenlem  7040  findcard2  7083  findcard2s  7084  findcard2sd  7086  unfiin  7123  f1finf1o  7151  fidcenumlemrk  7158  fidcenumlemr  7159  fidcenum  7160  sbthlemi6  7166  sbthlemi8  7168  elfi2  7176  supisolem  7212  enumct  7319  nninfninc  7327  ismkvnex  7359  exmidontriimlem4  7444  netap  7478  2omotaplemap  7481  cc2lem  7490  dfplpq2  7579  dfmpq2  7580  mulpipqqs  7598  distrnqg  7612  ltexnqq  7633  subhalfnqq  7639  prarloclemarch  7643  nnnq0lem1  7671  distrnq0  7684  npsspw  7696  prarloclemlo  7719  prarloclem3  7722  prarloclemcalc  7727  genplt2i  7735  distrlem1prl  7807  distrlem1pru  7808  distrlem4prl  7809  distrlem4pru  7810  ltprordil  7814  ltexprlemlol  7827  ltexprlemupu  7829  addextpr  7846  recexprlemopl  7850  recexprlemdisj  7855  recexprlem1ssl  7858  aptiprleml  7864  prsrlem1  7967  recexgt0sr  7998  addcnsr  8059  mulcnsr  8060  mulcnsrec  8068  axaddcl  8089  axmulcl  8091  axmulcom  8096  rereceu  8114  mpomulf  8174  ltntri  8312  cnegexlem1  8359  cnegex  8362  addsub4  8427  le2add  8629  lt2add  8630  lt2sub  8645  le2sub  8646  rereim  8771  apreim  8788  mulreim  8789  addext  8795  mulext  8799  receuap  8854  rec11ap  8895  rec11rap  8896  divdivdivap  8898  ddcanap  8911  divadddivap  8912  divsubdivap  8913  conjmulap  8914  rerecclap  8915  subrecap  9024  recgt0  9035  prodgt0gt0  9036  prodgt0  9037  prodge0  9039  ltmul12a  9045  lemul12a  9047  lemulge11  9051  lt2mul2div  9064  ltrec  9068  lerec  9069  lt2msq  9071  ltrec1  9073  le2msq  9086  msq11  9087  ledivp1  9088  mulle0r  9129  peano5uzti  9593  eluzuzle  9769  qreccl  9881  elpq  9888  xrltso  10036  z2ge  10066  xpncan  10111  xaddge0  10118  xle2add  10119  xleaddadd  10127  ixxss1  10144  ixxss2  10145  elioc2  10176  divelunit  10242  fzass4  10302  fzrev  10324  fzonmapblen  10432  elfzodifsumelfzo  10452  ssfzo12bi  10476  rebtwn2z  10520  qbtwnxr  10523  modqid  10617  modqcyc  10627  modqaddabs  10630  modqaddmod  10631  mulqaddmodid  10632  modqadd2mod  10642  modqltm1p1mod  10644  modqsubmod  10650  modqsubmodmod  10651  modqmulmod  10657  modqmulmodr  10658  modqsubdir  10661  frecuzrdgg  10684  nninfinf  10711  seq3val  10728  seqvalcd  10729  seq3feq  10748  seq3f1olemp  10783  seqfeq4g  10799  expp1  10814  expcl2lemap  10819  expnegzap  10841  expadd  10849  expmul  10852  leexp1a  10862  expnlbnd  10932  nn0ltexp2  10977  nn0opth2  10992  bcval  11017  bcval5  11031  bcpasc  11034  hashunsng  11077  seq3coll  11112  iswrdiz  11129  sswrd  11131  ccatalpha  11199  ccatw2s1p1g  11231  swrdwrdsymbg  11254  swrdsb0eq  11255  ccatswrd  11260  pfxf  11272  pfxwrdsymbg  11280  wrd2ind  11313  swrdccatin2  11319  pfxccatin12lem2  11321  pfxccatin12lem3  11322  pfxccatin12  11323  pfxccat3  11324  swrdccat  11325  shftfvalg  11401  shftfval  11404  seq3shft  11421  caucvgrelemrec  11562  resqrexlemdecn  11595  sqrtmul  11618  sqrtdiv  11625  leabs  11657  absexpzap  11663  ltabs  11670  abslt  11671  absle  11672  abssubap0  11673  amgm2  11701  icodiamlt  11763  qdenre  11785  maxleim  11788  maxleastlt  11798  rexico  11804  zmaxcl  11807  minmax  11813  xrmaxleastlt  11839  xrminmax  11848  climuni  11876  cn1lem  11897  iserex  11922  iserle  11925  climserle  11928  climcau  11930  summodclem2a  11965  summodc  11967  isumss  11975  fisumss  11976  fsumadd  11990  isumadd  12015  fsum2dlemstep  12018  fsum2d  12019  fisum0diag2  12031  fsumabs  12049  isumsplit  12075  geolim  12095  geo2lim  12100  geoisum  12101  geoisumr  12102  geoisum1  12103  mertenslemub  12118  mertenslemi1  12119  mertenslem2  12120  mertensabs  12121  prodmodclem2  12161  prodmodc  12162  zproddc  12163  fprodseq  12167  fprodcl2lem  12189  fprod2dlemstep  12206  fprodle  12224  fprodmodd  12225  efcvgfsum  12251  eftlcl  12272  reeftlcl  12273  tanaddap  12323  zdvdsdc  12396  dvds2ln  12408  dvdsle  12428  divconjdvds  12433  dvdsext  12439  bitsfzo  12539  gcdsupex  12551  gcdsupcl  12552  bezoutlemmain  12592  bezoutlemaz  12597  bezoutlembi  12599  bezout  12605  gcdmultiplez  12615  dvdsmulgcd  12619  bezoutr  12626  bezoutr1  12627  lcmval  12658  lcmcllem  12662  ncoprmgcdne1b  12684  cncongr1  12698  isprm5  12737  prmdvdsexp  12743  sqrt2irr  12757  pw2dvdslemn  12760  pw2dvdseu  12763  nonsq  12802  powm2modprm  12848  pcmul  12897  pcqmul  12899  pcexp  12905  pcneg  12921  pcdvdstr  12923  pcprmpw2  12929  pcfac  12946  expnprm  12949  prmpwdvds  12951  mul4sq  12990  ssnnctlemct  13090  infpn2  13100  isstruct2r  13116  setsfun  13140  setsfun0  13141  ismndd  13543  submnd0  13550  mhmf1o  13576  resmhm  13593  mhmco  13596  mhmima  13597  dfgrp2  13633  grprcan  13643  grplmulf1o  13680  grplactcnv  13708  pwssub  13719  mhmmnd  13726  mulgval  13732  mulgz  13760  mulgnn0dir  13762  mulgdir  13764  mulgneg2  13766  mhmmulg  13773  issubg4m  13803  nmzsubg  13820  ssnmz  13821  ghmmhmb  13864  resghm  13870  ghmpreima  13876  ghmnsgpreima  13879  ghmf1o  13885  eqgabl  13940  gsumfzconst  13951  rngpropd  13992  srglmhm  14030  srgrmhm  14031  isring  14037  ringadd2  14064  ringpropd  14075  ringlghm  14098  ringrghm  14099  oppr1g  14119  dvdsrex  14136  dvdsrtr  14139  issubrg  14259  unitrrg  14305  islmod  14329  islmodd  14331  lmodfopne  14364  lmodprop2d  14386  lssvacl  14403  lssvsubcl  14404  lssvscl  14413  islss3  14417  lsslss  14419  lss1d  14421  lsspropdg  14469  dflidl2rng  14519  gsumfzfsumlemm  14625  expghmap  14645  mulgghm2  14646  znval  14674  znunit  14697  znrrg  14698  psrbaglesuppg  14710  mplvalcoe  14733  neissex  14918  tgrest  14922  ssrest  14935  restopn2  14936  cnco  14974  cnss1  14979  cnss2  14980  cnptopresti  14991  uptx  15027  txrest  15029  psmetres2  15086  xmetres2  15132  xblss2ps  15157  blhalf  15161  blssexps  15182  blssex  15183  blin2  15185  blbas  15186  bdmetval  15253  metcnpi  15268  metcnpi2  15269  qtopbas  15275  tgqioo  15308  cncfss  15336  mulc1cncf  15342  cncfmptid  15350  dedekindicc  15386  ivthdec  15397  cnplimcim  15420  cnplimclemle  15421  cnplimccntop  15423  limccnp2cntop  15430  dvfgg  15441  dvcj  15462  dvrecap  15466  dvmptfsum  15478  dveflem  15479  elply2  15488  ply1termlem  15495  plymullem1  15501  eflt  15528  ptolemy  15577  cos11  15606  rpcxpmul2  15666  cxplt  15669  cxple  15670  cxplt3  15673  apcxp2  15692  rprelogbmul  15708  rprelogbdiv  15710  sgmval  15736  sgmval2  15737  sgmf  15739  sgmmul  15749  perfect  15754  lgsval2lem  15768  lgsdir2lem5  15790  2sqlem6  15878  umgrnloopv  15994  upgredg  16024  usgr1eop  16125  upgredginwlk  16236  wlkv0  16249  clwwlkccatlem  16280  2omap  16654  pw1map  16656  pwtrufal  16658  nninfalllem1  16673  nninfsellemqall  16680  nnnninfex  16687  sbthom  16693  qdencn  16694  isomninnlem  16701  trirec0  16715  apdiff  16719  qdiff  16720  iswomninnlem  16721  ismkvnnlem  16724  ltlenmkv  16742