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  1065  simp2ll  1069  simp3ll  1073  rmob  3102  ifnefals  3627  prneimg  3831  exmid01  4261  pwntru  4262  ordtri2or2exmidlem  4595  onsucelsucexmidlem  4598  poinxp  4765  mpteqb  5698  fvmptt  5699  fcof1  5880  acexmid  5973  dftpos4  6379  tfrlem3ag  6425  tfrlem3a  6426  tfrlemi1  6448  tfrexlem  6450  tfr1onlem3ag  6453  nntr2  6619  dcdifsnid  6620  qsel  6729  ecopovsymg  6751  ecopoverg  6753  th3qlem1  6754  mapss  6808  xpmapenlem  6978  findcard2  7019  findcard2s  7020  findcard2sd  7022  unfiin  7056  f1finf1o  7082  fidcenumlemrk  7089  fidcenumlemr  7090  fidcenum  7091  sbthlemi6  7097  sbthlemi8  7099  elfi2  7107  supisolem  7143  enumct  7250  nninfninc  7258  ismkvnex  7290  exmidontriimlem4  7374  netap  7408  2omotaplemap  7411  cc2lem  7420  dfplpq2  7509  dfmpq2  7510  mulpipqqs  7528  distrnqg  7542  ltexnqq  7563  subhalfnqq  7569  prarloclemarch  7573  nnnq0lem1  7601  distrnq0  7614  npsspw  7626  prarloclemlo  7649  prarloclem3  7652  prarloclemcalc  7657  genplt2i  7665  distrlem1prl  7737  distrlem1pru  7738  distrlem4prl  7739  distrlem4pru  7740  ltprordil  7744  ltexprlemlol  7757  ltexprlemupu  7759  addextpr  7776  recexprlemopl  7780  recexprlemdisj  7785  recexprlem1ssl  7788  aptiprleml  7794  prsrlem1  7897  recexgt0sr  7928  addcnsr  7989  mulcnsr  7990  mulcnsrec  7998  axaddcl  8019  axmulcl  8021  axmulcom  8026  rereceu  8044  mpomulf  8104  ltntri  8242  cnegexlem1  8289  cnegex  8292  addsub4  8357  le2add  8559  lt2add  8560  lt2sub  8575  le2sub  8576  rereim  8701  apreim  8718  mulreim  8719  addext  8725  mulext  8729  receuap  8784  rec11ap  8825  rec11rap  8826  divdivdivap  8828  ddcanap  8841  divadddivap  8842  divsubdivap  8843  conjmulap  8844  rerecclap  8845  subrecap  8954  recgt0  8965  prodgt0gt0  8966  prodgt0  8967  prodge0  8969  ltmul12a  8975  lemul12a  8977  lemulge11  8981  lt2mul2div  8994  ltrec  8998  lerec  8999  lt2msq  9001  ltrec1  9003  le2msq  9016  msq11  9017  ledivp1  9018  mulle0r  9059  peano5uzti  9523  eluzuzle  9698  qreccl  9805  elpq  9812  xrltso  9960  z2ge  9990  xpncan  10035  xaddge0  10042  xle2add  10043  xleaddadd  10051  ixxss1  10068  ixxss2  10069  elioc2  10100  divelunit  10166  fzass4  10226  fzrev  10248  fzonmapblen  10355  elfzodifsumelfzo  10374  ssfzo12bi  10398  rebtwn2z  10441  qbtwnxr  10444  modqid  10538  modqcyc  10548  modqaddabs  10551  modqaddmod  10552  mulqaddmodid  10553  modqadd2mod  10563  modqltm1p1mod  10565  modqsubmod  10571  modqsubmodmod  10572  modqmulmod  10578  modqmulmodr  10579  modqsubdir  10582  frecuzrdgg  10605  nninfinf  10632  seq3val  10649  seqvalcd  10650  seq3feq  10669  seq3f1olemp  10704  seqfeq4g  10720  expp1  10735  expcl2lemap  10740  expnegzap  10762  expadd  10770  expmul  10773  leexp1a  10783  expnlbnd  10853  nn0ltexp2  10898  nn0opth2  10913  bcval  10938  bcval5  10952  bcpasc  10955  hashunsng  10996  seq3coll  11031  iswrdiz  11045  sswrd  11047  swrdwrdsymbg  11162  swrdsb0eq  11163  ccatswrd  11168  pfxf  11180  pfxwrdsymbg  11188  wrd2ind  11221  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccatin12lem3  11230  pfxccatin12  11231  pfxccat3  11232  swrdccat  11233  shftfvalg  11295  shftfval  11298  seq3shft  11315  caucvgrelemrec  11456  resqrexlemdecn  11489  sqrtmul  11512  sqrtdiv  11519  leabs  11551  absexpzap  11557  ltabs  11564  abslt  11565  absle  11566  abssubap0  11567  amgm2  11595  icodiamlt  11657  qdenre  11679  maxleim  11682  maxleastlt  11692  rexico  11698  zmaxcl  11701  minmax  11707  xrmaxleastlt  11733  xrminmax  11742  climuni  11770  cn1lem  11791  iserex  11816  iserle  11819  climserle  11822  climcau  11824  summodclem2a  11858  summodc  11860  isumss  11868  fisumss  11869  fsumadd  11883  isumadd  11908  fsum2dlemstep  11911  fsum2d  11912  fisum0diag2  11924  fsumabs  11942  isumsplit  11968  geolim  11988  geo2lim  11993  geoisum  11994  geoisumr  11995  geoisum1  11996  mertenslemub  12011  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  prodmodclem2  12054  prodmodc  12055  zproddc  12056  fprodseq  12060  fprodcl2lem  12082  fprod2dlemstep  12099  fprodle  12117  fprodmodd  12118  efcvgfsum  12144  eftlcl  12165  reeftlcl  12166  tanaddap  12216  zdvdsdc  12289  dvds2ln  12301  dvdsle  12321  divconjdvds  12326  dvdsext  12332  bitsfzo  12432  gcdsupex  12444  gcdsupcl  12445  bezoutlemmain  12485  bezoutlemaz  12490  bezoutlembi  12492  bezout  12498  gcdmultiplez  12508  dvdsmulgcd  12512  bezoutr  12519  bezoutr1  12520  lcmval  12551  lcmcllem  12555  ncoprmgcdne1b  12577  cncongr1  12591  isprm5  12630  prmdvdsexp  12636  sqrt2irr  12650  pw2dvdslemn  12653  pw2dvdseu  12656  nonsq  12695  powm2modprm  12741  pcmul  12790  pcqmul  12792  pcexp  12798  pcneg  12814  pcdvdstr  12816  pcprmpw2  12822  pcfac  12839  expnprm  12842  prmpwdvds  12844  mul4sq  12883  ssnnctlemct  12983  infpn2  12993  isstruct2r  13009  setsfun  13033  setsfun0  13034  ismndd  13436  submnd0  13443  mhmf1o  13469  resmhm  13486  mhmco  13489  mhmima  13490  dfgrp2  13526  grprcan  13536  grplmulf1o  13573  grplactcnv  13601  pwssub  13612  mhmmnd  13619  mulgval  13625  mulgz  13653  mulgnn0dir  13655  mulgdir  13657  mulgneg2  13659  mhmmulg  13666  issubg4m  13696  nmzsubg  13713  ssnmz  13714  ghmmhmb  13757  resghm  13763  ghmpreima  13769  ghmnsgpreima  13772  ghmf1o  13778  eqgabl  13833  gsumfzconst  13844  rngpropd  13884  srglmhm  13922  srgrmhm  13923  isring  13929  ringadd2  13956  ringpropd  13967  ringlghm  13990  ringrghm  13991  oppr1g  14011  dvdsrex  14027  dvdsrtr  14030  issubrg  14150  unitrrg  14196  islmod  14220  islmodd  14222  lmodfopne  14255  lmodprop2d  14277  lssvacl  14294  lssvsubcl  14295  lssvscl  14304  islss3  14308  lsslss  14310  lss1d  14312  lsspropdg  14360  dflidl2rng  14410  gsumfzfsumlemm  14516  expghmap  14536  mulgghm2  14537  znval  14565  znunit  14588  znrrg  14589  psrbaglesuppg  14601  mplvalcoe  14619  neissex  14804  tgrest  14808  ssrest  14821  restopn2  14822  cnco  14860  cnss1  14865  cnss2  14866  cnptopresti  14877  uptx  14913  txrest  14915  psmetres2  14972  xmetres2  15018  xblss2ps  15043  blhalf  15047  blssexps  15068  blssex  15069  blin2  15071  blbas  15072  bdmetval  15139  metcnpi  15154  metcnpi2  15155  qtopbas  15161  tgqioo  15194  cncfss  15222  mulc1cncf  15228  cncfmptid  15236  dedekindicc  15272  ivthdec  15283  cnplimcim  15306  cnplimclemle  15307  cnplimccntop  15309  limccnp2cntop  15316  dvfgg  15327  dvcj  15348  dvrecap  15352  dvmptfsum  15364  dveflem  15365  elply2  15374  ply1termlem  15381  plymullem1  15387  eflt  15414  ptolemy  15463  cos11  15492  rpcxpmul2  15552  cxplt  15555  cxple  15556  cxplt3  15559  apcxp2  15578  rprelogbmul  15594  rprelogbdiv  15596  sgmval  15622  sgmval2  15623  sgmf  15625  sgmmul  15635  perfect  15640  lgsval2lem  15654  lgsdir2lem5  15676  2sqlem6  15764  umgrnloopv  15879  upgredg  15907  2omap  16270  pw1map  16272  pwtrufal  16274  nninfalllem1  16285  nninfsellemqall  16292  nnnninfex  16299  sbthom  16305  qdencn  16306  isomninnlem  16309  trirec0  16323  apdiff  16327  iswomninnlem  16328  ismkvnnlem  16331  ltlenmkv  16349