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  1062  simp2ll  1066  simp3ll  1070  rmob  3082  ifnefals  3604  prneimg  3805  exmid01  4232  pwntru  4233  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  poinxp  4733  mpteqb  5655  fvmptt  5656  fcof1  5833  acexmid  5924  dftpos4  6330  tfrlem3ag  6376  tfrlem3a  6377  tfrlemi1  6399  tfrexlem  6401  tfr1onlem3ag  6404  nntr2  6570  dcdifsnid  6571  qsel  6680  ecopovsymg  6702  ecopoverg  6704  th3qlem1  6705  mapss  6759  xpmapenlem  6919  findcard2  6959  findcard2s  6960  findcard2sd  6962  unfiin  6996  f1finf1o  7022  fidcenumlemrk  7029  fidcenumlemr  7030  fidcenum  7031  sbthlemi6  7037  sbthlemi8  7039  elfi2  7047  supisolem  7083  enumct  7190  nninfninc  7198  ismkvnex  7230  exmidontriimlem4  7309  netap  7339  2omotaplemap  7342  cc2lem  7351  dfplpq2  7440  dfmpq2  7441  mulpipqqs  7459  distrnqg  7473  ltexnqq  7494  subhalfnqq  7500  prarloclemarch  7504  nnnq0lem1  7532  distrnq0  7545  npsspw  7557  prarloclemlo  7580  prarloclem3  7583  prarloclemcalc  7588  genplt2i  7596  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  ltprordil  7675  ltexprlemlol  7688  ltexprlemupu  7690  addextpr  7707  recexprlemopl  7711  recexprlemdisj  7716  recexprlem1ssl  7719  aptiprleml  7725  prsrlem1  7828  recexgt0sr  7859  addcnsr  7920  mulcnsr  7921  mulcnsrec  7929  axaddcl  7950  axmulcl  7952  axmulcom  7957  rereceu  7975  mpomulf  8035  ltntri  8173  cnegexlem1  8220  cnegex  8223  addsub4  8288  le2add  8490  lt2add  8491  lt2sub  8506  le2sub  8507  rereim  8632  apreim  8649  mulreim  8650  addext  8656  mulext  8660  receuap  8715  rec11ap  8756  rec11rap  8757  divdivdivap  8759  ddcanap  8772  divadddivap  8773  divsubdivap  8774  conjmulap  8775  rerecclap  8776  subrecap  8885  recgt0  8896  prodgt0gt0  8897  prodgt0  8898  prodge0  8900  ltmul12a  8906  lemul12a  8908  lemulge11  8912  lt2mul2div  8925  ltrec  8929  lerec  8930  lt2msq  8932  ltrec1  8934  le2msq  8947  msq11  8948  ledivp1  8949  mulle0r  8990  peano5uzti  9453  eluzuzle  9628  qreccl  9735  elpq  9742  xrltso  9890  z2ge  9920  xpncan  9965  xaddge0  9972  xle2add  9973  xleaddadd  9981  ixxss1  9998  ixxss2  9999  elioc2  10030  divelunit  10096  fzass4  10156  fzrev  10178  fzonmapblen  10282  elfzodifsumelfzo  10296  ssfzo12bi  10320  rebtwn2z  10363  qbtwnxr  10366  modqid  10460  modqcyc  10470  modqaddabs  10473  modqaddmod  10474  mulqaddmodid  10475  modqadd2mod  10485  modqltm1p1mod  10487  modqsubmod  10493  modqsubmodmod  10494  modqmulmod  10500  modqmulmodr  10501  modqsubdir  10504  frecuzrdgg  10527  nninfinf  10554  seq3val  10571  seqvalcd  10572  seq3feq  10591  seq3f1olemp  10626  seqfeq4g  10642  expp1  10657  expcl2lemap  10662  expnegzap  10684  expadd  10692  expmul  10695  leexp1a  10705  expnlbnd  10775  nn0ltexp2  10820  nn0opth2  10835  bcval  10860  bcval5  10874  bcpasc  10877  hashunsng  10918  seq3coll  10953  iswrdiz  10961  sswrd  10963  shftfvalg  11002  shftfval  11005  seq3shft  11022  caucvgrelemrec  11163  resqrexlemdecn  11196  sqrtmul  11219  sqrtdiv  11226  leabs  11258  absexpzap  11264  ltabs  11271  abslt  11272  absle  11273  abssubap0  11274  amgm2  11302  icodiamlt  11364  qdenre  11386  maxleim  11389  maxleastlt  11399  rexico  11405  zmaxcl  11408  minmax  11414  xrmaxleastlt  11440  xrminmax  11449  climuni  11477  cn1lem  11498  iserex  11523  iserle  11526  climserle  11529  climcau  11531  summodclem2a  11565  summodc  11567  isumss  11575  fisumss  11576  fsumadd  11590  isumadd  11615  fsum2dlemstep  11618  fsum2d  11619  fisum0diag2  11631  fsumabs  11649  isumsplit  11675  geolim  11695  geo2lim  11700  geoisum  11701  geoisumr  11702  geoisum1  11703  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodcl2lem  11789  fprod2dlemstep  11806  fprodle  11824  fprodmodd  11825  efcvgfsum  11851  eftlcl  11872  reeftlcl  11873  tanaddap  11923  zdvdsdc  11996  dvds2ln  12008  dvdsle  12028  divconjdvds  12033  dvdsext  12039  bitsfzo  12139  gcdsupex  12151  gcdsupcl  12152  bezoutlemmain  12192  bezoutlemaz  12197  bezoutlembi  12199  bezout  12205  gcdmultiplez  12215  dvdsmulgcd  12219  bezoutr  12226  bezoutr1  12227  lcmval  12258  lcmcllem  12262  ncoprmgcdne1b  12284  cncongr1  12298  isprm5  12337  prmdvdsexp  12343  sqrt2irr  12357  pw2dvdslemn  12360  pw2dvdseu  12363  nonsq  12402  powm2modprm  12448  pcmul  12497  pcqmul  12499  pcexp  12505  pcneg  12521  pcdvdstr  12523  pcprmpw2  12529  pcfac  12546  expnprm  12549  prmpwdvds  12551  mul4sq  12590  ssnnctlemct  12690  infpn2  12700  isstruct2r  12716  setsfun  12740  setsfun0  12741  ismndd  13141  submnd0  13148  mhmf1o  13174  resmhm  13191  mhmco  13194  mhmima  13195  dfgrp2  13231  grprcan  13241  grplmulf1o  13278  grplactcnv  13306  pwssub  13317  mhmmnd  13324  mulgval  13330  mulgz  13358  mulgnn0dir  13360  mulgdir  13362  mulgneg2  13364  mhmmulg  13371  issubg4m  13401  nmzsubg  13418  ssnmz  13419  ghmmhmb  13462  resghm  13468  ghmpreima  13474  ghmnsgpreima  13477  ghmf1o  13483  eqgabl  13538  gsumfzconst  13549  rngpropd  13589  srglmhm  13627  srgrmhm  13628  isring  13634  ringadd2  13661  ringpropd  13672  ringlghm  13695  ringrghm  13696  oppr1g  13716  dvdsrex  13732  dvdsrtr  13735  issubrg  13855  unitrrg  13901  islmod  13925  islmodd  13927  lmodfopne  13960  lmodprop2d  13982  lssvacl  13999  lssvsubcl  14000  lssvscl  14009  islss3  14013  lsslss  14015  lss1d  14017  lsspropdg  14065  dflidl2rng  14115  gsumfzfsumlemm  14221  expghmap  14241  mulgghm2  14242  znval  14270  znunit  14293  znrrg  14294  psrbaglesuppg  14304  neissex  14487  tgrest  14491  ssrest  14504  restopn2  14505  cnco  14543  cnss1  14548  cnss2  14549  cnptopresti  14560  uptx  14596  txrest  14598  psmetres2  14655  xmetres2  14701  xblss2ps  14726  blhalf  14730  blssexps  14751  blssex  14752  blin2  14754  blbas  14755  bdmetval  14822  metcnpi  14837  metcnpi2  14838  qtopbas  14844  tgqioo  14877  cncfss  14905  mulc1cncf  14911  cncfmptid  14919  dedekindicc  14955  ivthdec  14966  cnplimcim  14989  cnplimclemle  14990  cnplimccntop  14992  limccnp2cntop  14999  dvfgg  15010  dvcj  15031  dvrecap  15035  dvmptfsum  15047  dveflem  15048  elply2  15057  ply1termlem  15064  plymullem1  15070  eflt  15097  ptolemy  15146  cos11  15175  rpcxpmul2  15235  cxplt  15238  cxple  15239  cxplt3  15242  apcxp2  15261  rprelogbmul  15277  rprelogbdiv  15279  sgmval  15305  sgmval2  15306  sgmf  15308  sgmmul  15318  perfect  15323  lgsval2lem  15337  lgsdir2lem5  15359  2sqlem6  15447  2omap  15728  pwtrufal  15730  nninfalllem1  15741  nninfsellemqall  15748  nnnninfex  15755  sbthom  15761  qdencn  15762  isomninnlem  15765  trirec0  15779  apdiff  15783  iswomninnlem  15784  ismkvnnlem  15787  ltlenmkv  15805