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  4335  pwntru  4336  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  poinxp  4844  mpteqb  5796  fvmptt  5797  fcof1  5989  acexmid  6084  fsuppeqg  6488  fvn0elsupp  6491  suppssdc  6500  suppssfvg  6503  dftpos4  6534  tfrlem3ag  6580  tfrlem3a  6581  tfrlemi1  6603  tfrexlem  6605  tfr1onlem3ag  6608  nntr2  6776  dcdifsnid  6777  qsel  6886  ecopovsymg  6908  ecopoverg  6910  th3qlem1  6911  mapss  6973  xpmapenlem  7149  findcard2  7193  findcard2s  7194  findcard2sd  7196  unfiin  7233  f1finf1o  7264  fidcenumlemrk  7271  fidcenumlemr  7272  fidcenum  7273  sbthlemi6  7279  sbthlemi8  7281  elfi2  7306  f1setfi  7317  2omap  7318  2omapfi  7320  supisolem  7348  enumct  7455  nninfninc  7463  ismkvnex  7495  exmidontriimlem4  7580  netap  7620  2omotaplemap  7623  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  ltexnqq  7775  subhalfnqq  7781  prarloclemarch  7785  nnnq0lem1  7813  distrnq0  7826  npsspw  7838  prarloclemlo  7861  prarloclem3  7864  prarloclemcalc  7869  genplt2i  7877  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemlol  7969  ltexprlemupu  7971  addextpr  7988  recexprlemopl  7992  recexprlemdisj  7997  recexprlem1ssl  8000  aptiprleml  8006  prsrlem1  8109  recexgt0sr  8140  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axaddcl  8231  axmulcl  8233  axmulcom  8238  rereceu  8256  mpomulf  8316  ltntri  8454  cnegexlem1  8501  cnegex  8504  addsub4  8569  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  rereim  8915  apreim  8932  mulreim  8933  addext  8939  mulext  8943  receuap  9000  rec11ap  9041  rec11rap  9042  divdivdivap  9044  ddcanap  9057  divadddivap  9058  divsubdivap  9059  conjmulap  9060  rerecclap  9061  subrecap  9170  recgt0  9181  prodgt0gt0  9182  prodgt0  9183  prodge0  9185  ltmul12a  9191  lemul12a  9193  lemulge11  9197  lt2mul2div  9210  ltrec  9214  lerec  9215  lt2msq  9217  ltrec1  9219  le2msq  9232  msq11  9233  ledivp1  9234  mulle0r  9275  peano5uzti  9756  eluzuzle  9932  qreccl  10044  elpq  10051  xrltso  10200  z2ge  10230  xpncan  10275  xaddge0  10282  xle2add  10283  xleaddadd  10291  ixxss1  10308  ixxss2  10309  elioc2  10340  divelunit  10406  fzass4  10470  fzrev  10493  fzonmapblen  10601  elfzodifsumelfzo  10621  ssfzo12bi  10645  rebtwn2z  10691  qbtwnxr  10694  modqid  10788  modqcyc  10798  modqaddabs  10801  modqaddmod  10802  mulqaddmodid  10803  modqadd2mod  10813  modqltm1p1mod  10815  modqsubmod  10821  modqsubmodmod  10822  modqmulmod  10828  modqmulmodr  10829  modqsubdir  10832  frecuzrdgg  10855  nninfinf  10882  seq3val  10899  seqvalcd  10900  seq3feq  10919  seq3f1olemp  10954  seqfeq4g  10970  expp1  10985  expcl2lemap  10990  expnegzap  11012  expadd  11020  expmul  11023  leexp1a  11033  resq01  11097  expnlbnd  11104  nn0ltexp2  11149  nn0opth2  11164  bcval  11189  bcval5  11203  bcpasc  11206  hashunsng  11250  sseqn  11281  hashfibclem  11284  hashfibc  11285  hashf1lem2  11288  seq3coll  11296  iswrdiz  11313  sswrd  11315  ccatalpha  11383  ccatw2s1p1g  11415  swrdwrdsymbg  11438  swrdsb0eq  11439  ccatswrd  11444  pfxf  11456  pfxwrdsymbg  11464  wrd2ind  11497  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccatin12  11507  pfxccat3  11508  swrdccat  11509  shftfvalg  11585  shftfval  11588  seq3shft  11605  caucvgrelemrec  11747  resqrexlemdecn  11780  sqrtmul  11803  sqrtdiv  11810  leabs  11842  absexpzap  11848  ltabs  11855  abslt  11856  absle  11857  abssubap0  11858  amgm2  11886  icodiamlt  11948  qdenre  11970  maxleim  11973  maxleastlt  11983  rexico  11989  zmaxcl  11992  minmax  11998  xrmaxleastlt  12024  xrminmax  12033  climuni  12061  cn1lem  12082  iserex  12107  iserle  12110  climserle  12113  climcau  12115  summodclem2a  12150  summodc  12152  isumss  12160  fisumss  12161  fsumadd  12175  isumadd  12200  fsum2dlemstep  12203  fsum2d  12204  fisum0diag2  12216  fsumabs  12234  isumsplit  12260  geolim  12280  geo2lim  12285  geoisum  12286  geoisumr  12287  geoisum1  12288  mertenslemub  12303  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  prodmodclem2  12346  prodmodc  12347  zproddc  12348  fprodseq  12352  fprodcl2lem  12374  fprod2dlemstep  12391  fprodle  12409  fprodmodd  12410  efcvgfsum  12436  eftlcl  12457  reeftlcl  12458  tanaddap  12508  zdvdsdc  12581  dvds2ln  12593  dvdsle  12613  divconjdvds  12618  dvdsext  12624  bitsfzo  12724  gcdsupex  12736  gcdsupcl  12737  bezoutlemmain  12777  bezoutlemaz  12782  bezoutlembi  12784  bezout  12790  gcdmultiplez  12800  dvdsmulgcd  12804  bezoutr  12811  bezoutr1  12812  lcmval  12843  lcmcllem  12847  ncoprmgcdne1b  12869  cncongr1  12883  isprm5  12922  prmdvdsexp  12928  sqrt2irr  12942  pw2dvdslemn  12945  pw2dvdseu  12948  nonsq  12987  powm2modprm  13033  pcmul  13082  pcqmul  13084  pcexp  13090  pcneg  13106  pcdvdstr  13108  pcprmpw2  13114  pcfac  13131  expnprm  13134  prmpwdvds  13136  mul4sq  13175  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemsima  13261  ssnnctlemct  13339  infpn2  13349  isstruct2r  13365  setsfun  13389  setsfun0  13390  ismndd  13752  submnd0  13759  mhmf1o  13779  resmhm  13796  mhmco  13799  mhmima  13800  dfgrp2  13834  grprcan  13844  grplmulf1o  13881  grplactcnv  13909  mhmmnd  13921  mulgval  13927  mulgz  13955  mulgnn0dir  13957  mulgdir  13959  mulgneg2  13961  mhmmulg  13968  issubg4m  13998  nmzsubg  14015  ssnmz  14016  ghmmhmb  14059  resghm  14065  ghmpreima  14071  ghmnsgpreima  14074  ghmf1o  14080  eqgabl  14136  gzsumconst  14145  pwssub  14218  rngpropd  14256  srglmhm  14299  srgrmhm  14300  isring  14306  ringadd2  14334  ringpropd  14345  ringlghm  14368  ringrghm  14369  oppr1g  14390  dvdsrex  14407  dvdsrtr  14410  issubrg  14531  unitrrg  14578  aprnzr  14601  opprdrng  14622  islmod  14629  islmodd  14631  lmodfopne  14665  lmodprop2d  14687  lssvacl  14704  lssvsubcl  14705  lssvscl  14714  islss3  14718  lsslss  14720  lss1d  14722  lsspropdg  14770  dflidl2rng  14820  expghmap  14944  mulgghm2  14945  znval  14973  znunit  14996  znrrg  14997  assapropd  15016  assamulgscmlem1  15043  assamulgscmlem2  15044  psrbaglesuppg  15059  mplvalcoe  15083  neissex  15268  tgrest  15272  ssrest  15285  restopn2  15286  cnco  15324  cnss1  15329  cnss2  15330  cnptopresti  15341  uptx  15377  txrest  15379  psmetres2  15436  xmetres2  15482  xblss2ps  15507  blhalf  15511  blssexps  15532  blssex  15533  blin2  15535  blbas  15536  bdmetval  15603  metcnpi  15618  metcnpi2  15619  qtopbas  15625  tgqioo  15658  cncfss  15686  mulc1cncf  15692  cncfmptid  15700  dedekindicc  15736  ivthdec  15747  cnplimcim  15770  cnplimclemle  15771  cnplimccntop  15773  limccnp2cntop  15780  dvfgg  15791  dvcj  15812  dvrecap  15816  dvmptfsum  15828  dveflem  15829  elply2  15838  ply1termlem  15845  plymullem1  15851  eflt  15878  ptolemy  15928  cos11  15957  logdivlt  15999  logdivle  16000  rpcxpmul2  16021  cxplt  16024  cxple  16025  cxplt3  16028  apcxp2  16047  rprelogbmul  16063  rprelogbdiv  16065  birthdaylem3  16095  pellexlem3  16099  sgmval  16103  sgmval2  16104  sgmf  16106  sgmmul  16116  perfect  16121  bcmax  16125  lgsval2lem  16141  lgsdir2lem5  16163  2sqlem6  16251  umgrnloopv  16367  upgredg  16397  usgr1eop  16498  upgredginwlk  16609  wlkv0  16622  clwwlkccatlem  16653  pw1map  17037  pwtrufal  17039  nninfalllem1  17063  nninfsellemqall  17070  nnnninfex  17077  sbthom  17083  qdencn  17084  isomninnlem  17091  trirec0  17105  apdiff  17109  qdiff  17110  iswomninnlem  17111  ismkvnnlem  17114  ltlenmkv  17132