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  1060  simp2ll  1064  simp3ll  1068  rmob  3055  prneimg  3774  exmid01  4198  pwntru  4199  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  poinxp  4695  mpteqb  5606  fvmptt  5607  fcof1  5783  acexmid  5873  dftpos4  6263  tfrlem3ag  6309  tfrlem3a  6310  tfrlemi1  6332  tfrexlem  6334  tfr1onlem3ag  6337  nntr2  6503  dcdifsnid  6504  qsel  6611  ecopovsymg  6633  ecopoverg  6635  th3qlem1  6636  mapss  6690  xpmapenlem  6848  findcard2  6888  findcard2s  6889  findcard2sd  6891  unfiin  6924  f1finf1o  6945  fidcenumlemrk  6952  fidcenumlemr  6953  fidcenum  6954  sbthlemi6  6960  sbthlemi8  6962  elfi2  6970  supisolem  7006  enumct  7113  ismkvnex  7152  exmidontriimlem4  7222  netap  7252  2omotaplemap  7255  cc2lem  7264  dfplpq2  7352  dfmpq2  7353  mulpipqqs  7371  distrnqg  7385  ltexnqq  7406  subhalfnqq  7412  prarloclemarch  7416  nnnq0lem1  7444  distrnq0  7457  npsspw  7469  prarloclemlo  7492  prarloclem3  7495  prarloclemcalc  7500  genplt2i  7508  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  ltprordil  7587  ltexprlemlol  7600  ltexprlemupu  7602  addextpr  7619  recexprlemopl  7623  recexprlemdisj  7628  recexprlem1ssl  7631  aptiprleml  7637  prsrlem1  7740  recexgt0sr  7771  addcnsr  7832  mulcnsr  7833  mulcnsrec  7841  axaddcl  7862  axmulcl  7864  axmulcom  7869  rereceu  7887  ltntri  8084  cnegexlem1  8131  cnegex  8134  addsub4  8199  le2add  8400  lt2add  8401  lt2sub  8416  le2sub  8417  rereim  8542  apreim  8559  mulreim  8560  addext  8566  mulext  8570  receuap  8625  rec11ap  8666  rec11rap  8667  divdivdivap  8669  ddcanap  8682  divadddivap  8683  divsubdivap  8684  conjmulap  8685  rerecclap  8686  subrecap  8795  recgt0  8806  prodgt0gt0  8807  prodgt0  8808  prodge0  8810  ltmul12a  8816  lemul12a  8818  lemulge11  8822  lt2mul2div  8835  ltrec  8839  lerec  8840  lt2msq  8842  ltrec1  8844  le2msq  8857  msq11  8858  ledivp1  8859  mulle0r  8900  peano5uzti  9360  eluzuzle  9535  qreccl  9641  elpq  9647  xrltso  9795  z2ge  9825  xpncan  9870  xaddge0  9877  xle2add  9878  xleaddadd  9886  ixxss1  9903  ixxss2  9904  elioc2  9935  divelunit  10001  fzass4  10061  fzrev  10083  fzonmapblen  10186  elfzodifsumelfzo  10200  ssfzo12bi  10224  rebtwn2z  10254  qbtwnxr  10257  modqid  10348  modqcyc  10358  modqaddabs  10361  modqaddmod  10362  mulqaddmodid  10363  modqadd2mod  10373  modqltm1p1mod  10375  modqsubmod  10381  modqsubmodmod  10382  modqmulmod  10388  modqmulmodr  10389  modqsubdir  10392  frecuzrdgg  10415  seq3val  10457  seqvalcd  10458  seq3feq  10471  seq3f1olemp  10501  expp1  10526  expcl2lemap  10531  expnegzap  10553  expadd  10561  expmul  10564  leexp1a  10574  expnlbnd  10644  nn0ltexp2  10688  nn0opth2  10703  bcval  10728  bcval5  10742  bcpasc  10745  hashunsng  10786  seq3coll  10821  shftfvalg  10826  shftfval  10829  seq3shft  10846  caucvgrelemrec  10987  resqrexlemdecn  11020  sqrtmul  11043  sqrtdiv  11050  leabs  11082  absexpzap  11088  ltabs  11095  abslt  11096  absle  11097  abssubap0  11098  amgm2  11126  icodiamlt  11188  qdenre  11210  maxleim  11213  maxleastlt  11223  rexico  11229  zmaxcl  11232  minmax  11237  xrmaxleastlt  11263  xrminmax  11272  climuni  11300  cn1lem  11321  iserex  11346  iserle  11349  climserle  11352  climcau  11354  summodclem2a  11388  summodc  11390  isumss  11398  fisumss  11399  fsumadd  11413  isumadd  11438  fsum2dlemstep  11441  fsum2d  11442  fisum0diag2  11454  fsumabs  11472  isumsplit  11498  geolim  11518  geo2lim  11523  geoisum  11524  geoisumr  11525  geoisum1  11526  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodseq  11590  fprodcl2lem  11612  fprod2dlemstep  11629  fprodle  11647  fprodmodd  11648  efcvgfsum  11674  eftlcl  11695  reeftlcl  11696  tanaddap  11746  zdvdsdc  11818  dvds2ln  11830  dvdsle  11849  divconjdvds  11854  dvdsext  11860  gcdsupex  11957  gcdsupcl  11958  bezoutlemmain  11998  bezoutlemaz  12003  bezoutlembi  12005  bezout  12011  gcdmultiplez  12021  dvdsmulgcd  12025  bezoutr  12032  bezoutr1  12033  lcmval  12062  lcmcllem  12066  ncoprmgcdne1b  12088  cncongr1  12102  isprm5  12141  prmdvdsexp  12147  sqrt2irr  12161  pw2dvdslemn  12164  pw2dvdseu  12167  nonsq  12206  powm2modprm  12251  pcmul  12300  pcqmul  12302  pcexp  12308  pcneg  12323  pcdvdstr  12325  pcprmpw2  12331  pcfac  12347  expnprm  12350  prmpwdvds  12352  mul4sq  12391  ssnnctlemct  12446  infpn2  12456  isstruct2r  12472  setsfun  12496  setsfun0  12497  ismndd  12837  submnd0  12844  mhmf1o  12860  mhmco  12873  mhmima  12874  dfgrp2  12901  grprcan  12909  grplmulf1o  12943  grplactcnv  12971  mhmmnd  12979  mulgval  12985  mulgz  13009  mulgnn0dir  13011  mulgdir  13013  mulgneg2  13015  mhmmulg  13022  issubg4m  13051  nmzsubg  13068  ssnmz  13069  srglmhm  13174  srgrmhm  13175  isring  13181  ringadd2  13208  ringpropd  13215  oppr1g  13250  dvdsrex  13265  dvdsrtr  13268  issubrg  13340  islmod  13379  islmodd  13381  neissex  13635  tgrest  13639  ssrest  13652  restopn2  13653  cnco  13691  cnss1  13696  cnss2  13697  cnptopresti  13708  uptx  13744  txrest  13746  psmetres2  13803  xmetres2  13849  xblss2ps  13874  blhalf  13878  blssexps  13899  blssex  13900  blin2  13902  blbas  13903  bdmetval  13970  metcnpi  13985  metcnpi2  13986  qtopbas  13992  tgqioo  14017  cncfss  14040  mulc1cncf  14046  cncfmptid  14053  dedekindicc  14081  ivthdec  14092  cnplimcim  14106  cnplimclemle  14107  cnplimccntop  14109  limccnp2cntop  14116  dvfgg  14127  dvcj  14143  dvrecap  14147  dveflem  14157  eflt  14166  ptolemy  14215  cos11  14244  cxplt  14306  cxple  14307  cxplt3  14310  apcxp2  14328  rprelogbmul  14343  rprelogbdiv  14345  lgsval2lem  14381  lgsdir2lem5  14403  2sqlem6  14437  pwtrufal  14717  nninfalllem1  14727  nninfsellemqall  14734  sbthom  14744  qdencn  14745  isomninnlem  14748  trirec0  14762  apdiff  14766  iswomninnlem  14767  ismkvnnlem  14770  ltlenmkv  14787