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  1087  simp2ll  1091  simp3ll  1095  rmob  3135  ifnefals  3666  prneimg  3877  exmid01  4310  pwntru  4311  ordtri2or2exmidlem  4647  onsucelsucexmidlem  4650  poinxp  4818  mpteqb  5767  fvmptt  5768  fcof1  5955  acexmid  6048  fsuppeqg  6447  fvn0elsupp  6450  suppssdc  6459  suppssfvg  6462  dftpos4  6493  tfrlem3ag  6539  tfrlem3a  6540  tfrlemi1  6562  tfrexlem  6564  tfr1onlem3ag  6567  nntr2  6735  dcdifsnid  6736  qsel  6845  ecopovsymg  6867  ecopoverg  6869  th3qlem1  6870  mapss  6925  xpmapenlem  7101  findcard2  7145  findcard2s  7146  findcard2sd  7148  unfiin  7185  f1finf1o  7216  fidcenumlemrk  7223  fidcenumlemr  7224  fidcenum  7225  sbthlemi6  7231  sbthlemi8  7233  elfi2  7258  2omap  7268  2omapfi  7270  supisolem  7298  enumct  7405  nninfninc  7413  ismkvnex  7445  exmidontriimlem4  7530  netap  7564  2omotaplemap  7567  cc2lem  7576  dfplpq2  7665  dfmpq2  7666  mulpipqqs  7684  distrnqg  7698  ltexnqq  7719  subhalfnqq  7725  prarloclemarch  7729  nnnq0lem1  7757  distrnq0  7770  npsspw  7782  prarloclemlo  7805  prarloclem3  7808  prarloclemcalc  7813  genplt2i  7821  distrlem1prl  7893  distrlem1pru  7894  distrlem4prl  7895  distrlem4pru  7896  ltprordil  7900  ltexprlemlol  7913  ltexprlemupu  7915  addextpr  7932  recexprlemopl  7936  recexprlemdisj  7941  recexprlem1ssl  7944  aptiprleml  7950  prsrlem1  8053  recexgt0sr  8084  addcnsr  8145  mulcnsr  8146  mulcnsrec  8154  axaddcl  8175  axmulcl  8177  axmulcom  8182  rereceu  8200  mpomulf  8260  ltntri  8397  cnegexlem1  8444  cnegex  8447  addsub4  8512  le2add  8714  lt2add  8715  lt2sub  8730  le2sub  8731  rereim  8856  apreim  8873  mulreim  8874  addext  8880  mulext  8884  receuap  8939  rec11ap  8980  rec11rap  8981  divdivdivap  8983  ddcanap  8996  divadddivap  8997  divsubdivap  8998  conjmulap  8999  rerecclap  9000  subrecap  9109  recgt0  9120  prodgt0gt0  9121  prodgt0  9122  prodge0  9124  ltmul12a  9130  lemul12a  9132  lemulge11  9136  lt2mul2div  9149  ltrec  9153  lerec  9154  lt2msq  9156  ltrec1  9158  le2msq  9171  msq11  9172  ledivp1  9173  mulle0r  9214  peano5uzti  9682  eluzuzle  9858  qreccl  9970  elpq  9977  xrltso  10125  z2ge  10155  xpncan  10200  xaddge0  10207  xle2add  10208  xleaddadd  10216  ixxss1  10233  ixxss2  10234  elioc2  10265  divelunit  10331  fzass4  10392  fzrev  10414  fzonmapblen  10522  elfzodifsumelfzo  10542  ssfzo12bi  10566  rebtwn2z  10610  qbtwnxr  10613  modqid  10707  modqcyc  10717  modqaddabs  10720  modqaddmod  10721  mulqaddmodid  10722  modqadd2mod  10732  modqltm1p1mod  10734  modqsubmod  10740  modqsubmodmod  10741  modqmulmod  10747  modqmulmodr  10748  modqsubdir  10751  frecuzrdgg  10774  nninfinf  10801  seq3val  10818  seqvalcd  10819  seq3feq  10838  seq3f1olemp  10873  seqfeq4g  10889  expp1  10904  expcl2lemap  10909  expnegzap  10931  expadd  10939  expmul  10942  leexp1a  10952  expnlbnd  11022  nn0ltexp2  11067  nn0opth2  11082  bcval  11107  bcval5  11121  bcpasc  11124  hashunsng  11167  sseqn  11196  hashfibclem  11199  hashfibc  11200  seq3coll  11207  iswrdiz  11224  sswrd  11226  ccatalpha  11294  ccatw2s1p1g  11326  swrdwrdsymbg  11349  swrdsb0eq  11350  ccatswrd  11355  pfxf  11367  pfxwrdsymbg  11375  wrd2ind  11408  swrdccatin2  11414  pfxccatin12lem2  11416  pfxccatin12lem3  11417  pfxccatin12  11418  pfxccat3  11419  swrdccat  11420  shftfvalg  11496  shftfval  11499  seq3shft  11516  caucvgrelemrec  11657  resqrexlemdecn  11690  sqrtmul  11713  sqrtdiv  11720  leabs  11752  absexpzap  11758  ltabs  11765  abslt  11766  absle  11767  abssubap0  11768  amgm2  11796  icodiamlt  11858  qdenre  11880  maxleim  11883  maxleastlt  11893  rexico  11899  zmaxcl  11902  minmax  11908  xrmaxleastlt  11934  xrminmax  11943  climuni  11971  cn1lem  11992  iserex  12017  iserle  12020  climserle  12023  climcau  12025  summodclem2a  12060  summodc  12062  isumss  12070  fisumss  12071  fsumadd  12085  isumadd  12110  fsum2dlemstep  12113  fsum2d  12114  fisum0diag2  12126  fsumabs  12144  isumsplit  12170  geolim  12190  geo2lim  12195  geoisum  12196  geoisumr  12197  geoisum1  12198  mertenslemub  12213  mertenslemi1  12214  mertenslem2  12215  mertensabs  12216  prodmodclem2  12256  prodmodc  12257  zproddc  12258  fprodseq  12262  fprodcl2lem  12284  fprod2dlemstep  12301  fprodle  12319  fprodmodd  12320  efcvgfsum  12346  eftlcl  12367  reeftlcl  12368  tanaddap  12418  zdvdsdc  12491  dvds2ln  12503  dvdsle  12523  divconjdvds  12528  dvdsext  12534  bitsfzo  12634  gcdsupex  12646  gcdsupcl  12647  bezoutlemmain  12687  bezoutlemaz  12692  bezoutlembi  12694  bezout  12700  gcdmultiplez  12710  dvdsmulgcd  12714  bezoutr  12721  bezoutr1  12722  lcmval  12753  lcmcllem  12757  ncoprmgcdne1b  12779  cncongr1  12793  isprm5  12832  prmdvdsexp  12838  sqrt2irr  12852  pw2dvdslemn  12855  pw2dvdseu  12858  nonsq  12897  powm2modprm  12943  pcmul  12992  pcqmul  12994  pcexp  13000  pcneg  13016  pcdvdstr  13018  pcprmpw2  13024  pcfac  13041  expnprm  13044  prmpwdvds  13046  mul4sq  13085  ssnnctlemct  13186  infpn2  13196  isstruct2r  13212  setsfun  13236  setsfun0  13237  ismndd  13639  submnd0  13646  mhmf1o  13672  resmhm  13689  mhmco  13692  mhmima  13693  dfgrp2  13729  grprcan  13739  grplmulf1o  13776  grplactcnv  13804  pwssub  13815  mhmmnd  13822  mulgval  13828  mulgz  13856  mulgnn0dir  13858  mulgdir  13860  mulgneg2  13862  mhmmulg  13869  issubg4m  13899  nmzsubg  13916  ssnmz  13917  ghmmhmb  13960  resghm  13966  ghmpreima  13972  ghmnsgpreima  13975  ghmf1o  13981  eqgabl  14036  gsumfzconst  14047  rngpropd  14088  srglmhm  14126  srgrmhm  14127  isring  14133  ringadd2  14160  ringpropd  14171  ringlghm  14194  ringrghm  14195  oppr1g  14215  dvdsrex  14232  dvdsrtr  14235  issubrg  14355  unitrrg  14402  islmod  14426  islmodd  14428  lmodfopne  14461  lmodprop2d  14483  lssvacl  14500  lssvsubcl  14501  lssvscl  14510  islss3  14514  lsslss  14516  lss1d  14518  lsspropdg  14566  dflidl2rng  14616  gsumfzfsumlemm  14722  expghmap  14742  mulgghm2  14743  znval  14771  znunit  14794  znrrg  14795  psrbaglesuppg  14808  mplvalcoe  14832  neissex  15017  tgrest  15021  ssrest  15034  restopn2  15035  cnco  15073  cnss1  15078  cnss2  15079  cnptopresti  15090  uptx  15126  txrest  15128  psmetres2  15185  xmetres2  15231  xblss2ps  15256  blhalf  15260  blssexps  15281  blssex  15282  blin2  15284  blbas  15285  bdmetval  15352  metcnpi  15367  metcnpi2  15368  qtopbas  15374  tgqioo  15407  cncfss  15435  mulc1cncf  15441  cncfmptid  15449  dedekindicc  15485  ivthdec  15496  cnplimcim  15519  cnplimclemle  15520  cnplimccntop  15522  limccnp2cntop  15529  dvfgg  15540  dvcj  15561  dvrecap  15565  dvmptfsum  15577  dveflem  15578  elply2  15587  ply1termlem  15594  plymullem1  15600  eflt  15627  ptolemy  15676  cos11  15705  rpcxpmul2  15765  cxplt  15768  cxple  15769  cxplt3  15772  apcxp2  15791  rprelogbmul  15807  rprelogbdiv  15809  pellexlem3  15834  sgmval  15838  sgmval2  15839  sgmf  15841  sgmmul  15851  perfect  15856  lgsval2lem  15870  lgsdir2lem5  15892  2sqlem6  15980  umgrnloopv  16096  upgredg  16126  usgr1eop  16227  upgredginwlk  16338  wlkv0  16351  clwwlkccatlem  16382  pw1map  16756  pwtrufal  16758  nninfalllem1  16773  nninfsellemqall  16780  nnnninfex  16787  sbthom  16793  qdencn  16794  isomninnlem  16801  trirec0  16815  apdiff  16819  qdiff  16820  iswomninnlem  16821  ismkvnnlem  16824  ltlenmkv  16842