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  1062  simp2ll  1066  simp3ll  1070  rmob  3082  ifnefals  3603  prneimg  3804  exmid01  4231  pwntru  4232  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  poinxp  4732  mpteqb  5652  fvmptt  5653  fcof1  5830  acexmid  5921  dftpos4  6321  tfrlem3ag  6367  tfrlem3a  6368  tfrlemi1  6390  tfrexlem  6392  tfr1onlem3ag  6395  nntr2  6561  dcdifsnid  6562  qsel  6671  ecopovsymg  6693  ecopoverg  6695  th3qlem1  6696  mapss  6750  xpmapenlem  6910  findcard2  6950  findcard2s  6951  findcard2sd  6953  unfiin  6987  f1finf1o  7013  fidcenumlemrk  7020  fidcenumlemr  7021  fidcenum  7022  sbthlemi6  7028  sbthlemi8  7030  elfi2  7038  supisolem  7074  enumct  7181  nninfninc  7189  ismkvnex  7221  exmidontriimlem4  7291  netap  7321  2omotaplemap  7324  cc2lem  7333  dfplpq2  7421  dfmpq2  7422  mulpipqqs  7440  distrnqg  7454  ltexnqq  7475  subhalfnqq  7481  prarloclemarch  7485  nnnq0lem1  7513  distrnq0  7526  npsspw  7538  prarloclemlo  7561  prarloclem3  7564  prarloclemcalc  7569  genplt2i  7577  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  ltprordil  7656  ltexprlemlol  7669  ltexprlemupu  7671  addextpr  7688  recexprlemopl  7692  recexprlemdisj  7697  recexprlem1ssl  7700  aptiprleml  7706  prsrlem1  7809  recexgt0sr  7840  addcnsr  7901  mulcnsr  7902  mulcnsrec  7910  axaddcl  7931  axmulcl  7933  axmulcom  7938  rereceu  7956  mpomulf  8016  ltntri  8154  cnegexlem1  8201  cnegex  8204  addsub4  8269  le2add  8471  lt2add  8472  lt2sub  8487  le2sub  8488  rereim  8613  apreim  8630  mulreim  8631  addext  8637  mulext  8641  receuap  8696  rec11ap  8737  rec11rap  8738  divdivdivap  8740  ddcanap  8753  divadddivap  8754  divsubdivap  8755  conjmulap  8756  rerecclap  8757  subrecap  8866  recgt0  8877  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  ltmul12a  8887  lemul12a  8889  lemulge11  8893  lt2mul2div  8906  ltrec  8910  lerec  8911  lt2msq  8913  ltrec1  8915  le2msq  8928  msq11  8929  ledivp1  8930  mulle0r  8971  peano5uzti  9434  eluzuzle  9609  qreccl  9716  elpq  9723  xrltso  9871  z2ge  9901  xpncan  9946  xaddge0  9953  xle2add  9954  xleaddadd  9962  ixxss1  9979  ixxss2  9980  elioc2  10011  divelunit  10077  fzass4  10137  fzrev  10159  fzonmapblen  10263  elfzodifsumelfzo  10277  ssfzo12bi  10301  rebtwn2z  10344  qbtwnxr  10347  modqid  10441  modqcyc  10451  modqaddabs  10454  modqaddmod  10455  mulqaddmodid  10456  modqadd2mod  10466  modqltm1p1mod  10468  modqsubmod  10474  modqsubmodmod  10475  modqmulmod  10481  modqmulmodr  10482  modqsubdir  10485  frecuzrdgg  10508  nninfinf  10535  seq3val  10552  seqvalcd  10553  seq3feq  10572  seq3f1olemp  10607  seqfeq4g  10623  expp1  10638  expcl2lemap  10643  expnegzap  10665  expadd  10673  expmul  10676  leexp1a  10686  expnlbnd  10756  nn0ltexp2  10801  nn0opth2  10816  bcval  10841  bcval5  10855  bcpasc  10858  hashunsng  10899  seq3coll  10934  iswrdiz  10942  sswrd  10944  shftfvalg  10983  shftfval  10986  seq3shft  11003  caucvgrelemrec  11144  resqrexlemdecn  11177  sqrtmul  11200  sqrtdiv  11207  leabs  11239  absexpzap  11245  ltabs  11252  abslt  11253  absle  11254  abssubap0  11255  amgm2  11283  icodiamlt  11345  qdenre  11367  maxleim  11370  maxleastlt  11380  rexico  11386  zmaxcl  11389  minmax  11395  xrmaxleastlt  11421  xrminmax  11430  climuni  11458  cn1lem  11479  iserex  11504  iserle  11507  climserle  11510  climcau  11512  summodclem2a  11546  summodc  11548  isumss  11556  fisumss  11557  fsumadd  11571  isumadd  11596  fsum2dlemstep  11599  fsum2d  11600  fisum0diag2  11612  fsumabs  11630  isumsplit  11656  geolim  11676  geo2lim  11681  geoisum  11682  geoisumr  11683  geoisum1  11684  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodcl2lem  11770  fprod2dlemstep  11787  fprodle  11805  fprodmodd  11806  efcvgfsum  11832  eftlcl  11853  reeftlcl  11854  tanaddap  11904  zdvdsdc  11977  dvds2ln  11989  dvdsle  12009  divconjdvds  12014  dvdsext  12020  bitsfzo  12119  gcdsupex  12124  gcdsupcl  12125  bezoutlemmain  12165  bezoutlemaz  12170  bezoutlembi  12172  bezout  12178  gcdmultiplez  12188  dvdsmulgcd  12192  bezoutr  12199  bezoutr1  12200  lcmval  12231  lcmcllem  12235  ncoprmgcdne1b  12257  cncongr1  12271  isprm5  12310  prmdvdsexp  12316  sqrt2irr  12330  pw2dvdslemn  12333  pw2dvdseu  12336  nonsq  12375  powm2modprm  12421  pcmul  12470  pcqmul  12472  pcexp  12478  pcneg  12494  pcdvdstr  12496  pcprmpw2  12502  pcfac  12519  expnprm  12522  prmpwdvds  12524  mul4sq  12563  ssnnctlemct  12663  infpn2  12673  isstruct2r  12689  setsfun  12713  setsfun0  12714  ismndd  13078  submnd0  13085  mhmf1o  13102  resmhm  13119  mhmco  13122  mhmima  13123  dfgrp2  13159  grprcan  13169  grplmulf1o  13206  grplactcnv  13234  mhmmnd  13246  mulgval  13252  mulgz  13280  mulgnn0dir  13282  mulgdir  13284  mulgneg2  13286  mhmmulg  13293  issubg4m  13323  nmzsubg  13340  ssnmz  13341  ghmmhmb  13384  resghm  13390  ghmpreima  13396  ghmnsgpreima  13399  ghmf1o  13405  eqgabl  13460  gsumfzconst  13471  rngpropd  13511  srglmhm  13549  srgrmhm  13550  isring  13556  ringadd2  13583  ringpropd  13594  ringlghm  13617  ringrghm  13618  oppr1g  13638  dvdsrex  13654  dvdsrtr  13657  issubrg  13777  unitrrg  13823  islmod  13847  islmodd  13849  lmodfopne  13882  lmodprop2d  13904  lssvacl  13921  lssvsubcl  13922  lssvscl  13931  islss3  13935  lsslss  13937  lss1d  13939  lsspropdg  13987  dflidl2rng  14037  gsumfzfsumlemm  14143  expghmap  14163  mulgghm2  14164  znval  14192  znunit  14215  znrrg  14216  psrbaglesuppg  14226  neissex  14401  tgrest  14405  ssrest  14418  restopn2  14419  cnco  14457  cnss1  14462  cnss2  14463  cnptopresti  14474  uptx  14510  txrest  14512  psmetres2  14569  xmetres2  14615  xblss2ps  14640  blhalf  14644  blssexps  14665  blssex  14666  blin2  14668  blbas  14669  bdmetval  14736  metcnpi  14751  metcnpi2  14752  qtopbas  14758  tgqioo  14791  cncfss  14819  mulc1cncf  14825  cncfmptid  14833  dedekindicc  14869  ivthdec  14880  cnplimcim  14903  cnplimclemle  14904  cnplimccntop  14906  limccnp2cntop  14913  dvfgg  14924  dvcj  14945  dvrecap  14949  dvmptfsum  14961  dveflem  14962  elply2  14971  ply1termlem  14978  plymullem1  14984  eflt  15011  ptolemy  15060  cos11  15089  rpcxpmul2  15149  cxplt  15152  cxple  15153  cxplt3  15156  apcxp2  15175  rprelogbmul  15191  rprelogbdiv  15193  sgmval  15219  sgmval2  15220  sgmf  15222  sgmmul  15232  perfect  15237  lgsval2lem  15251  lgsdir2lem5  15273  2sqlem6  15361  pwtrufal  15642  nninfalllem1  15652  nninfsellemqall  15659  sbthom  15670  qdencn  15671  isomninnlem  15674  trirec0  15688  apdiff  15692  iswomninnlem  15693  ismkvnnlem  15696  ltlenmkv  15714