Theorem simpll 531

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 492	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1ll  1091  simp2ll  1095  simp3ll  1099  rmob  3145  ifnefals  3685  ifeqeqxdc  3687  prneimg  3899  exmid01  4337  pwntru  4338  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  poinxp  4846  mpteqb  5799  fvmptt  5800  fcof1  5992  acexmid  6087  fsuppeqg  6492  fvn0elsupp  6495  suppssdc  6504  suppssfvg  6507  dftpos4  6538  tfrlem3ag  6584  tfrlem3a  6585  tfrlemi1  6607  tfrexlem  6609  tfr1onlem3ag  6612  nntr2  6780  dcdifsnid  6781  qsel  6890  ecopovsymg  6912  ecopoverg  6914  th3qlem1  6915  mapss  6978  xpmapenlem  7154  findcard2  7198  findcard2s  7199  findcard2sd  7201  unfiin  7238  f1finf1o  7270  fidcenumlemrk  7277  fidcenumlemr  7278  fidcenum  7279  sbthlemi6  7285  sbthlemi8  7287  elfi2  7312  f1setfi  7323  2omap  7325  2omapfi  7327  supisolem  7355  enumct  7462  nninfninc  7470  ismkvnex  7502  exmidontriimlem4  7587  netap  7627  2omotaplemap  7630  cc2lem  7639  dfplpq2  7728  dfmpq2  7729  mulpipqqs  7747  distrnqg  7761  ltexnqq  7782  subhalfnqq  7788  prarloclemarch  7792  nnnq0lem1  7820  distrnq0  7833  npsspw  7845  prarloclemlo  7868  prarloclem3  7871  prarloclemcalc  7876  genplt2i  7884  distrlem1prl  7956  distrlem1pru  7957  distrlem4prl  7958  distrlem4pru  7959  ltprordil  7963  ltexprlemlol  7976  ltexprlemupu  7978  addextpr  7995  recexprlemopl  7999  recexprlemdisj  8004  recexprlem1ssl  8007  aptiprleml  8013  prsrlem1  8116  recexgt0sr  8147  addcnsr  8208  mulcnsr  8209  mulcnsrec  8217  axaddcl  8238  axmulcl  8240  axmulcom  8245  rereceu  8263  mpomulf  8323  ltntri  8462  cnegexlem1  8509  cnegex  8512  addsub4  8577  le2add  8780  lt2add  8781  lt2sub  8796  le2sub  8797  rereim  8923  apreim  8940  mulreim  8941  addext  8947  mulext  8951  receuap  9008  rec11ap  9049  rec11rap  9050  divdivdivap  9052  ddcanap  9065  divadddivap  9066  divsubdivap  9067  conjmulap  9068  rerecclap  9069  subrecap  9178  recgt0  9189  prodgt0gt0  9190  prodgt0  9191  prodge0  9193  ltmul12a  9199  lemul12a  9201  lemulge11  9205  lt2mul2div  9218  ltrec  9222  lerec  9223  lt2msq  9225  ltrec1  9227  le2msq  9240  msq11  9241  ledivp1  9242  mulle0r  9283  peano5uzti  9766  eluzuzle  9947  qreccl  10059  irraddap  10064  elpq  10067  xrltso  10216  z2ge  10246  xpncan  10291  xaddge0  10298  xle2add  10299  xleaddadd  10307  ixxss1  10324  ixxss2  10325  elioc2  10356  divelunit  10422  fzass4  10486  fzrev  10509  fzonmapblen  10617  elfzodifsumelfzo  10637  ssfzo12bi  10661  rebtwn2z  10707  qbtwnxr  10710  flaplt  10740  modqid  10808  modqcyc  10818  modqaddabs  10821  modqaddmod  10822  mulqaddmodid  10823  modqadd2mod  10833  modqltm1p1mod  10835  modqsubmod  10841  modqsubmodmod  10842  modqmulmod  10848  modqmulmodr  10849  modqsubdir  10852  frecuzrdgg  10875  nninfinf  10902  seq3val  10919  seqvalcd  10920  seq3feq  10939  seq3f1olemp  10974  seqfeq4g  10990  expp1  11005  expcl2lemap  11010  expnegzap  11032  expadd  11040  expmul  11043  leexp1a  11053  resq01  11117  expnlbnd  11124  nn0ltexp2  11170  nn0opth2  11185  bcval  11210  bcval5  11224  bcpasc  11227  hashunsng  11271  sseqn  11302  hashfibclem  11305  hashfibc  11306  hashf1lem2  11309  seq3coll  11317  iswrdiz  11334  sswrd  11336  ccatalpha  11404  ccatw2s1p1g  11436  swrdwrdsymbg  11459  swrdsb0eq  11460  ccatswrd  11465  pfxf  11477  pfxwrdsymbg  11485  wrd2ind  11518  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12lem3  11527  pfxccatin12  11528  pfxccat3  11529  swrdccat  11530  shftfvalg  11606  shftfval  11609  seq3shft  11626  caucvgrelemrec  11768  resqrexlemdecn  11801  sqrtmul  11824  sqrtdiv  11831  leabs  11863  absexpzap  11870  ltabs  11877  abslt  11878  absle  11879  abssubap0  11880  amgm2  11908  icodiamlt  11970  qdenre  11992  maxleim  11995  maxleastlt  12005  rexico  12011  zmaxcl  12014  minmax  12021  zmincl  12030  xrmaxleastlt  12048  xrminmax  12057  climuni  12085  cn1lem  12106  iserex  12131  iserle  12134  climserle  12137  climcau  12139  summodclem2a  12174  summodc  12176  isumss  12184  fisumss  12185  fsumadd  12199  isumadd  12224  fsum2dlemstep  12227  fsum2d  12228  fisum0diag2  12240  fsumabs  12258  isumsplit  12284  geolim  12304  geo2lim  12309  geoisum  12310  geoisumr  12311  geoisum1  12312  mertenslemub  12327  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  prodmodclem2  12370  prodmodc  12371  zproddc  12372  fprodseq  12376  fprodcl2lem  12398  fprod2dlemstep  12415  fprodle  12433  fprodmodd  12434  efcvgfsum  12460  eftlcl  12481  reeftlcl  12482  tanaddap  12532  zdvdsdc  12605  dvds2ln  12617  dvdsle  12637  divconjdvds  12642  dvdsext  12648  bitsfzo  12748  gcdsupex  12760  gcdsupcl  12761  bezoutlemmain  12801  bezoutlemaz  12806  bezoutlembi  12808  bezout  12814  gcdmultiplez  12824  dvdsmulgcd  12828  bezoutr  12835  bezoutr1  12836  lcmval  12867  lcmcllem  12871  ncoprmgcdne1b  12893  cncongr1  12907  isprm5  12947  prmdvdsexp  12953  sqrt2irr  12967  pwbdvdslemn  12970  nonsq  13013  powm2modprm  13061  pcmul  13110  pcqmul  13112  pcexp  13118  pcneg  13134  pcdvdstr  13136  pcprmpw2  13142  pcfac  13159  expnprm  13162  prmpwdvds  13164  mul4sq  13203  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemsima  13318  ssnnctlemct  13396  infpn2  13406  isstruct2r  13422  setsfun  13446  setsfun0  13447  ismndd  13810  submnd0  13817  mhmf1o  13837  resmhm  13854  mhmco  13857  mhmima  13858  dfgrp2  13892  grprcan  13902  grplmulf1o  13939  grplactcnv  13967  mhmmnd  13979  mulgval  13985  mulgz  14013  mulgnn0dir  14015  mulgdir  14017  mulgneg2  14019  mhmmulg  14026  issubg4m  14056  nmzsubg  14073  ssnmz  14074  ghmmhmb  14117  resghm  14123  ghmpreima  14129  ghmnsgpreima  14132  ghmf1o  14138  resscntz  14167  cntzsgrpcl  14168  cntzsubm  14171  cntzsubg  14172  cntzmhm  14174  eqgabl  14225  gzsumconst  14234  gsumsnfdcmn  14258  pwssub  14324  rngpropd  14362  srglmhm  14405  srgrmhm  14406  isring  14412  ringadd2  14440  ringpropd  14451  ringlghm  14474  ringrghm  14475  oppr1g  14498  dvdsrex  14515  dvdsrtr  14518  issubrg  14639  unitrrg  14686  aprnzr  14709  opprdrng  14730  islmod  14737  islmodd  14739  lmodfopne  14773  lmodprop2d  14795  lssvacl  14812  lssvsubcl  14813  lssvscl  14822  islss3  14826  lsslss  14828  lss1d  14830  lsspropdg  14878  dflidl2rng  14928  expghmap  15052  mulgghm2  15053  znval  15081  znunit  15104  znrrg  15105  assapropd  15124  assamulgscmlem1  15151  assamulgscmlem2  15152  psrbaglesuppg  15172  mplvalcoe  15218  neissex  15403  tgrest  15407  ssrest  15420  restopn2  15421  cnco  15459  cnss1  15464  cnss2  15465  cnptopresti  15476  uptx  15512  txrest  15514  psmetres2  15571  xmetres2  15617  xblss2ps  15642  blhalf  15646  blssexps  15667  blssex  15668  blin2  15670  blbas  15671  bdmetval  15738  metcnpi  15753  metcnpi2  15754  qtopbas  15760  tgqioo  15793  cncfss  15821  mulc1cncf  15827  cncfmptid  15835  dedekindicc  15871  ivthdec  15882  cnplimcim  15905  cnplimclemle  15906  cnplimccntop  15908  limccnp2cntop  15915  dvfgg  15926  dvcj  15947  dvrecap  15951  dvmptfsum  15963  dveflem  15964  elply2  15973  ply1termlem  15980  plymullem1  15986  eflt  16013  ptolemy  16063  cos11  16093  logdivlt  16136  logdivle  16137  rpcxpmul2  16158  rpcxpmul2z  16160  cxplt  16163  cxple  16164  cxplt3  16167  apcxp2  16186  rprelogbmul  16203  rprelogbdiv  16205  birthdaylem3  16239  pellexlem3  16243  efnnfsumcl  16251  sgmval  16264  sgmval2  16265  sgmf  16267  efchtqdvds  16277  sgmmul  16302  perfect  16313  bcmax  16317  bposlem1  16323  bpos  16332  lgsval2lem  16346  lgsdir2lem5  16368  2sqlem6  16456  umgrnloopv  16572  upgredg  16602  usgr1eop  16703  upgredginwlk  16814  wlkv0  16827  clwwlkccatlem  16858  pw1map  17242  pwtrufal  17244  nninfalllem1  17269  nninfsellemqall  17276  nnnninfex  17283  sbthom  17289  qdencn  17290  isomninnlem  17297  trirec0  17312  apdiff  17316  qdiff  17317  iswomninnlem  17318  ismkvnnlem  17321  ltlenmkv  17339