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  1084  simp2ll  1088  simp3ll  1092  rmob  3122  ifnefals  3647  prneimg  3852  exmid01  4283  pwntru  4284  ordtri2or2exmidlem  4619  onsucelsucexmidlem  4622  poinxp  4790  mpteqb  5730  fvmptt  5731  fcof1  5916  acexmid  6009  dftpos4  6420  tfrlem3ag  6466  tfrlem3a  6467  tfrlemi1  6489  tfrexlem  6491  tfr1onlem3ag  6494  nntr2  6662  dcdifsnid  6663  qsel  6772  ecopovsymg  6794  ecopoverg  6796  th3qlem1  6797  mapss  6851  xpmapenlem  7023  findcard2  7064  findcard2s  7065  findcard2sd  7067  unfiin  7104  f1finf1o  7130  fidcenumlemrk  7137  fidcenumlemr  7138  fidcenum  7139  sbthlemi6  7145  sbthlemi8  7147  elfi2  7155  supisolem  7191  enumct  7298  nninfninc  7306  ismkvnex  7338  exmidontriimlem4  7422  netap  7456  2omotaplemap  7459  cc2lem  7468  dfplpq2  7557  dfmpq2  7558  mulpipqqs  7576  distrnqg  7590  ltexnqq  7611  subhalfnqq  7617  prarloclemarch  7621  nnnq0lem1  7649  distrnq0  7662  npsspw  7674  prarloclemlo  7697  prarloclem3  7700  prarloclemcalc  7705  genplt2i  7713  distrlem1prl  7785  distrlem1pru  7786  distrlem4prl  7787  distrlem4pru  7788  ltprordil  7792  ltexprlemlol  7805  ltexprlemupu  7807  addextpr  7824  recexprlemopl  7828  recexprlemdisj  7833  recexprlem1ssl  7836  aptiprleml  7842  prsrlem1  7945  recexgt0sr  7976  addcnsr  8037  mulcnsr  8038  mulcnsrec  8046  axaddcl  8067  axmulcl  8069  axmulcom  8074  rereceu  8092  mpomulf  8152  ltntri  8290  cnegexlem1  8337  cnegex  8340  addsub4  8405  le2add  8607  lt2add  8608  lt2sub  8623  le2sub  8624  rereim  8749  apreim  8766  mulreim  8767  addext  8773  mulext  8777  receuap  8832  rec11ap  8873  rec11rap  8874  divdivdivap  8876  ddcanap  8889  divadddivap  8890  divsubdivap  8891  conjmulap  8892  rerecclap  8893  subrecap  9002  recgt0  9013  prodgt0gt0  9014  prodgt0  9015  prodge0  9017  ltmul12a  9023  lemul12a  9025  lemulge11  9029  lt2mul2div  9042  ltrec  9046  lerec  9047  lt2msq  9049  ltrec1  9051  le2msq  9064  msq11  9065  ledivp1  9066  mulle0r  9107  peano5uzti  9571  eluzuzle  9747  qreccl  9854  elpq  9861  xrltso  10009  z2ge  10039  xpncan  10084  xaddge0  10091  xle2add  10092  xleaddadd  10100  ixxss1  10117  ixxss2  10118  elioc2  10149  divelunit  10215  fzass4  10275  fzrev  10297  fzonmapblen  10404  elfzodifsumelfzo  10424  ssfzo12bi  10448  rebtwn2z  10491  qbtwnxr  10494  modqid  10588  modqcyc  10598  modqaddabs  10601  modqaddmod  10602  mulqaddmodid  10603  modqadd2mod  10613  modqltm1p1mod  10615  modqsubmod  10621  modqsubmodmod  10622  modqmulmod  10628  modqmulmodr  10629  modqsubdir  10632  frecuzrdgg  10655  nninfinf  10682  seq3val  10699  seqvalcd  10700  seq3feq  10719  seq3f1olemp  10754  seqfeq4g  10770  expp1  10785  expcl2lemap  10790  expnegzap  10812  expadd  10820  expmul  10823  leexp1a  10833  expnlbnd  10903  nn0ltexp2  10948  nn0opth2  10963  bcval  10988  bcval5  11002  bcpasc  11005  hashunsng  11047  seq3coll  11082  iswrdiz  11096  sswrd  11098  ccatalpha  11166  swrdwrdsymbg  11217  swrdsb0eq  11218  ccatswrd  11223  pfxf  11235  pfxwrdsymbg  11243  wrd2ind  11276  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccatin12  11286  pfxccat3  11287  swrdccat  11288  shftfvalg  11350  shftfval  11353  seq3shft  11370  caucvgrelemrec  11511  resqrexlemdecn  11544  sqrtmul  11567  sqrtdiv  11574  leabs  11606  absexpzap  11612  ltabs  11619  abslt  11620  absle  11621  abssubap0  11622  amgm2  11650  icodiamlt  11712  qdenre  11734  maxleim  11737  maxleastlt  11747  rexico  11753  zmaxcl  11756  minmax  11762  xrmaxleastlt  11788  xrminmax  11797  climuni  11825  cn1lem  11846  iserex  11871  iserle  11874  climserle  11877  climcau  11879  summodclem2a  11913  summodc  11915  isumss  11923  fisumss  11924  fsumadd  11938  isumadd  11963  fsum2dlemstep  11966  fsum2d  11967  fisum0diag2  11979  fsumabs  11997  isumsplit  12023  geolim  12043  geo2lim  12048  geoisum  12049  geoisumr  12050  geoisum1  12051  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodseq  12115  fprodcl2lem  12137  fprod2dlemstep  12154  fprodle  12172  fprodmodd  12173  efcvgfsum  12199  eftlcl  12220  reeftlcl  12221  tanaddap  12271  zdvdsdc  12344  dvds2ln  12356  dvdsle  12376  divconjdvds  12381  dvdsext  12387  bitsfzo  12487  gcdsupex  12499  gcdsupcl  12500  bezoutlemmain  12540  bezoutlemaz  12545  bezoutlembi  12547  bezout  12553  gcdmultiplez  12563  dvdsmulgcd  12567  bezoutr  12574  bezoutr1  12575  lcmval  12606  lcmcllem  12610  ncoprmgcdne1b  12632  cncongr1  12646  isprm5  12685  prmdvdsexp  12691  sqrt2irr  12705  pw2dvdslemn  12708  pw2dvdseu  12711  nonsq  12750  powm2modprm  12796  pcmul  12845  pcqmul  12847  pcexp  12853  pcneg  12869  pcdvdstr  12871  pcprmpw2  12877  pcfac  12894  expnprm  12897  prmpwdvds  12899  mul4sq  12938  ssnnctlemct  13038  infpn2  13048  isstruct2r  13064  setsfun  13088  setsfun0  13089  ismndd  13491  submnd0  13498  mhmf1o  13524  resmhm  13541  mhmco  13544  mhmima  13545  dfgrp2  13581  grprcan  13591  grplmulf1o  13628  grplactcnv  13656  pwssub  13667  mhmmnd  13674  mulgval  13680  mulgz  13708  mulgnn0dir  13710  mulgdir  13712  mulgneg2  13714  mhmmulg  13721  issubg4m  13751  nmzsubg  13768  ssnmz  13769  ghmmhmb  13812  resghm  13818  ghmpreima  13824  ghmnsgpreima  13827  ghmf1o  13833  eqgabl  13888  gsumfzconst  13899  rngpropd  13939  srglmhm  13977  srgrmhm  13978  isring  13984  ringadd2  14011  ringpropd  14022  ringlghm  14045  ringrghm  14046  oppr1g  14066  dvdsrex  14083  dvdsrtr  14086  issubrg  14206  unitrrg  14252  islmod  14276  islmodd  14278  lmodfopne  14311  lmodprop2d  14333  lssvacl  14350  lssvsubcl  14351  lssvscl  14360  islss3  14364  lsslss  14366  lss1d  14368  lsspropdg  14416  dflidl2rng  14466  gsumfzfsumlemm  14572  expghmap  14592  mulgghm2  14593  znval  14621  znunit  14644  znrrg  14645  psrbaglesuppg  14657  mplvalcoe  14675  neissex  14860  tgrest  14864  ssrest  14877  restopn2  14878  cnco  14916  cnss1  14921  cnss2  14922  cnptopresti  14933  uptx  14969  txrest  14971  psmetres2  15028  xmetres2  15074  xblss2ps  15099  blhalf  15103  blssexps  15124  blssex  15125  blin2  15127  blbas  15128  bdmetval  15195  metcnpi  15210  metcnpi2  15211  qtopbas  15217  tgqioo  15250  cncfss  15278  mulc1cncf  15284  cncfmptid  15292  dedekindicc  15328  ivthdec  15339  cnplimcim  15362  cnplimclemle  15363  cnplimccntop  15365  limccnp2cntop  15372  dvfgg  15383  dvcj  15404  dvrecap  15408  dvmptfsum  15420  dveflem  15421  elply2  15430  ply1termlem  15437  plymullem1  15443  eflt  15470  ptolemy  15519  cos11  15548  rpcxpmul2  15608  cxplt  15611  cxple  15612  cxplt3  15615  apcxp2  15634  rprelogbmul  15650  rprelogbdiv  15652  sgmval  15678  sgmval2  15679  sgmf  15681  sgmmul  15691  perfect  15696  lgsval2lem  15710  lgsdir2lem5  15732  2sqlem6  15820  umgrnloopv  15935  upgredg  15963  usgr1eop  16064  upgredginwlk  16128  wlkv0  16141  clwwlkccatlem  16169  2omap  16472  pw1map  16474  pwtrufal  16476  nninfalllem1  16488  nninfsellemqall  16495  nnnninfex  16502  sbthom  16508  qdencn  16509  isomninnlem  16512  trirec0  16526  apdiff  16530  iswomninnlem  16531  ismkvnnlem  16534  ltlenmkv  16552