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  1084  simp2ll  1088  simp3ll  1092  rmob  3123  ifnefals  3648  prneimg  3855  exmid01  4286  pwntru  4287  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  poinxp  4793  mpteqb  5733  fvmptt  5734  fcof1  5919  acexmid  6012  dftpos4  6424  tfrlem3ag  6470  tfrlem3a  6471  tfrlemi1  6493  tfrexlem  6495  tfr1onlem3ag  6498  nntr2  6666  dcdifsnid  6667  qsel  6776  ecopovsymg  6798  ecopoverg  6800  th3qlem1  6801  mapss  6855  xpmapenlem  7030  findcard2  7073  findcard2s  7074  findcard2sd  7076  unfiin  7113  f1finf1o  7140  fidcenumlemrk  7147  fidcenumlemr  7148  fidcenum  7149  sbthlemi6  7155  sbthlemi8  7157  elfi2  7165  supisolem  7201  enumct  7308  nninfninc  7316  ismkvnex  7348  exmidontriimlem4  7432  netap  7466  2omotaplemap  7469  cc2lem  7478  dfplpq2  7567  dfmpq2  7568  mulpipqqs  7586  distrnqg  7600  ltexnqq  7621  subhalfnqq  7627  prarloclemarch  7631  nnnq0lem1  7659  distrnq0  7672  npsspw  7684  prarloclemlo  7707  prarloclem3  7710  prarloclemcalc  7715  genplt2i  7723  distrlem1prl  7795  distrlem1pru  7796  distrlem4prl  7797  distrlem4pru  7798  ltprordil  7802  ltexprlemlol  7815  ltexprlemupu  7817  addextpr  7834  recexprlemopl  7838  recexprlemdisj  7843  recexprlem1ssl  7846  aptiprleml  7852  prsrlem1  7955  recexgt0sr  7986  addcnsr  8047  mulcnsr  8048  mulcnsrec  8056  axaddcl  8077  axmulcl  8079  axmulcom  8084  rereceu  8102  mpomulf  8162  ltntri  8300  cnegexlem1  8347  cnegex  8350  addsub4  8415  le2add  8617  lt2add  8618  lt2sub  8633  le2sub  8634  rereim  8759  apreim  8776  mulreim  8777  addext  8783  mulext  8787  receuap  8842  rec11ap  8883  rec11rap  8884  divdivdivap  8886  ddcanap  8899  divadddivap  8900  divsubdivap  8901  conjmulap  8902  rerecclap  8903  subrecap  9012  recgt0  9023  prodgt0gt0  9024  prodgt0  9025  prodge0  9027  ltmul12a  9033  lemul12a  9035  lemulge11  9039  lt2mul2div  9052  ltrec  9056  lerec  9057  lt2msq  9059  ltrec1  9061  le2msq  9074  msq11  9075  ledivp1  9076  mulle0r  9117  peano5uzti  9581  eluzuzle  9757  qreccl  9869  elpq  9876  xrltso  10024  z2ge  10054  xpncan  10099  xaddge0  10106  xle2add  10107  xleaddadd  10115  ixxss1  10132  ixxss2  10133  elioc2  10164  divelunit  10230  fzass4  10290  fzrev  10312  fzonmapblen  10419  elfzodifsumelfzo  10439  ssfzo12bi  10463  rebtwn2z  10507  qbtwnxr  10510  modqid  10604  modqcyc  10614  modqaddabs  10617  modqaddmod  10618  mulqaddmodid  10619  modqadd2mod  10629  modqltm1p1mod  10631  modqsubmod  10637  modqsubmodmod  10638  modqmulmod  10644  modqmulmodr  10645  modqsubdir  10648  frecuzrdgg  10671  nninfinf  10698  seq3val  10715  seqvalcd  10716  seq3feq  10735  seq3f1olemp  10770  seqfeq4g  10786  expp1  10801  expcl2lemap  10806  expnegzap  10828  expadd  10836  expmul  10839  leexp1a  10849  expnlbnd  10919  nn0ltexp2  10964  nn0opth2  10979  bcval  11004  bcval5  11018  bcpasc  11021  hashunsng  11064  seq3coll  11099  iswrdiz  11113  sswrd  11115  ccatalpha  11183  ccatw2s1p1g  11215  swrdwrdsymbg  11238  swrdsb0eq  11239  ccatswrd  11244  pfxf  11256  pfxwrdsymbg  11264  wrd2ind  11297  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccatin12  11307  pfxccat3  11308  swrdccat  11309  shftfvalg  11372  shftfval  11375  seq3shft  11392  caucvgrelemrec  11533  resqrexlemdecn  11566  sqrtmul  11589  sqrtdiv  11596  leabs  11628  absexpzap  11634  ltabs  11641  abslt  11642  absle  11643  abssubap0  11644  amgm2  11672  icodiamlt  11734  qdenre  11756  maxleim  11759  maxleastlt  11769  rexico  11775  zmaxcl  11778  minmax  11784  xrmaxleastlt  11810  xrminmax  11819  climuni  11847  cn1lem  11868  iserex  11893  iserle  11896  climserle  11899  climcau  11901  summodclem2a  11935  summodc  11937  isumss  11945  fisumss  11946  fsumadd  11960  isumadd  11985  fsum2dlemstep  11988  fsum2d  11989  fisum0diag2  12001  fsumabs  12019  isumsplit  12045  geolim  12065  geo2lim  12070  geoisum  12071  geoisumr  12072  geoisum1  12073  mertenslemub  12088  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodseq  12137  fprodcl2lem  12159  fprod2dlemstep  12176  fprodle  12194  fprodmodd  12195  efcvgfsum  12221  eftlcl  12242  reeftlcl  12243  tanaddap  12293  zdvdsdc  12366  dvds2ln  12378  dvdsle  12398  divconjdvds  12403  dvdsext  12409  bitsfzo  12509  gcdsupex  12521  gcdsupcl  12522  bezoutlemmain  12562  bezoutlemaz  12567  bezoutlembi  12569  bezout  12575  gcdmultiplez  12585  dvdsmulgcd  12589  bezoutr  12596  bezoutr1  12597  lcmval  12628  lcmcllem  12632  ncoprmgcdne1b  12654  cncongr1  12668  isprm5  12707  prmdvdsexp  12713  sqrt2irr  12727  pw2dvdslemn  12730  pw2dvdseu  12733  nonsq  12772  powm2modprm  12818  pcmul  12867  pcqmul  12869  pcexp  12875  pcneg  12891  pcdvdstr  12893  pcprmpw2  12899  pcfac  12916  expnprm  12919  prmpwdvds  12921  mul4sq  12960  ssnnctlemct  13060  infpn2  13070  isstruct2r  13086  setsfun  13110  setsfun0  13111  ismndd  13513  submnd0  13520  mhmf1o  13546  resmhm  13563  mhmco  13566  mhmima  13567  dfgrp2  13603  grprcan  13613  grplmulf1o  13650  grplactcnv  13678  pwssub  13689  mhmmnd  13696  mulgval  13702  mulgz  13730  mulgnn0dir  13732  mulgdir  13734  mulgneg2  13736  mhmmulg  13743  issubg4m  13773  nmzsubg  13790  ssnmz  13791  ghmmhmb  13834  resghm  13840  ghmpreima  13846  ghmnsgpreima  13849  ghmf1o  13855  eqgabl  13910  gsumfzconst  13921  rngpropd  13961  srglmhm  13999  srgrmhm  14000  isring  14006  ringadd2  14033  ringpropd  14044  ringlghm  14067  ringrghm  14068  oppr1g  14088  dvdsrex  14105  dvdsrtr  14108  issubrg  14228  unitrrg  14274  islmod  14298  islmodd  14300  lmodfopne  14333  lmodprop2d  14355  lssvacl  14372  lssvsubcl  14373  lssvscl  14382  islss3  14386  lsslss  14388  lss1d  14390  lsspropdg  14438  dflidl2rng  14488  gsumfzfsumlemm  14594  expghmap  14614  mulgghm2  14615  znval  14643  znunit  14666  znrrg  14667  psrbaglesuppg  14679  mplvalcoe  14697  neissex  14882  tgrest  14886  ssrest  14899  restopn2  14900  cnco  14938  cnss1  14943  cnss2  14944  cnptopresti  14955  uptx  14991  txrest  14993  psmetres2  15050  xmetres2  15096  xblss2ps  15121  blhalf  15125  blssexps  15146  blssex  15147  blin2  15149  blbas  15150  bdmetval  15217  metcnpi  15232  metcnpi2  15233  qtopbas  15239  tgqioo  15272  cncfss  15300  mulc1cncf  15306  cncfmptid  15314  dedekindicc  15350  ivthdec  15361  cnplimcim  15384  cnplimclemle  15385  cnplimccntop  15387  limccnp2cntop  15394  dvfgg  15405  dvcj  15426  dvrecap  15430  dvmptfsum  15442  dveflem  15443  elply2  15452  ply1termlem  15459  plymullem1  15465  eflt  15492  ptolemy  15541  cos11  15570  rpcxpmul2  15630  cxplt  15633  cxple  15634  cxplt3  15637  apcxp2  15656  rprelogbmul  15672  rprelogbdiv  15674  sgmval  15700  sgmval2  15701  sgmf  15703  sgmmul  15713  perfect  15718  lgsval2lem  15732  lgsdir2lem5  15754  2sqlem6  15842  umgrnloopv  15958  upgredg  15988  usgr1eop  16089  upgredginwlk  16167  wlkv0  16180  clwwlkccatlem  16209  2omap  16544  pw1map  16546  pwtrufal  16548  nninfalllem1  16560  nninfsellemqall  16567  nnnninfex  16574  sbthom  16580  qdencn  16581  isomninnlem  16584  trirec0  16598  apdiff  16602  iswomninnlem  16603  ismkvnnlem  16606  ltlenmkv  16624