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  1087  simp2ll  1091  simp3ll  1095  rmob  3138  ifnefals  3669  prneimg  3880  exmid01  4313  pwntru  4314  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  poinxp  4821  mpteqb  5770  fvmptt  5771  fcof1  5958  acexmid  6051  fsuppeqg  6450  fvn0elsupp  6453  suppssdc  6462  suppssfvg  6465  dftpos4  6496  tfrlem3ag  6542  tfrlem3a  6543  tfrlemi1  6565  tfrexlem  6567  tfr1onlem3ag  6570  nntr2  6738  dcdifsnid  6739  qsel  6848  ecopovsymg  6870  ecopoverg  6872  th3qlem1  6873  mapss  6928  xpmapenlem  7104  findcard2  7148  findcard2s  7149  findcard2sd  7151  unfiin  7188  f1finf1o  7219  fidcenumlemrk  7226  fidcenumlemr  7227  fidcenum  7228  sbthlemi6  7234  sbthlemi8  7236  elfi2  7261  2omap  7271  2omapfi  7273  supisolem  7301  enumct  7408  nninfninc  7416  ismkvnex  7448  exmidontriimlem4  7533  netap  7573  2omotaplemap  7576  cc2lem  7585  dfplpq2  7674  dfmpq2  7675  mulpipqqs  7693  distrnqg  7707  ltexnqq  7728  subhalfnqq  7734  prarloclemarch  7738  nnnq0lem1  7766  distrnq0  7779  npsspw  7791  prarloclemlo  7814  prarloclem3  7817  prarloclemcalc  7822  genplt2i  7830  distrlem1prl  7902  distrlem1pru  7903  distrlem4prl  7904  distrlem4pru  7905  ltprordil  7909  ltexprlemlol  7922  ltexprlemupu  7924  addextpr  7941  recexprlemopl  7945  recexprlemdisj  7950  recexprlem1ssl  7953  aptiprleml  7959  prsrlem1  8062  recexgt0sr  8093  addcnsr  8154  mulcnsr  8155  mulcnsrec  8163  axaddcl  8184  axmulcl  8186  axmulcom  8191  rereceu  8209  mpomulf  8269  ltntri  8406  cnegexlem1  8453  cnegex  8456  addsub4  8521  le2add  8723  lt2add  8724  lt2sub  8739  le2sub  8740  rereim  8865  apreim  8882  mulreim  8883  addext  8889  mulext  8893  receuap  8948  rec11ap  8989  rec11rap  8990  divdivdivap  8992  ddcanap  9005  divadddivap  9006  divsubdivap  9007  conjmulap  9008  rerecclap  9009  subrecap  9118  recgt0  9129  prodgt0gt0  9130  prodgt0  9131  prodge0  9133  ltmul12a  9139  lemul12a  9141  lemulge11  9145  lt2mul2div  9158  ltrec  9162  lerec  9163  lt2msq  9165  ltrec1  9167  le2msq  9180  msq11  9181  ledivp1  9182  mulle0r  9223  peano5uzti  9692  eluzuzle  9868  qreccl  9980  elpq  9987  xrltso  10135  z2ge  10165  xpncan  10210  xaddge0  10217  xle2add  10218  xleaddadd  10226  ixxss1  10243  ixxss2  10244  elioc2  10275  divelunit  10341  fzass4  10402  fzrev  10425  fzonmapblen  10533  elfzodifsumelfzo  10553  ssfzo12bi  10577  rebtwn2z  10621  qbtwnxr  10624  modqid  10718  modqcyc  10728  modqaddabs  10731  modqaddmod  10732  mulqaddmodid  10733  modqadd2mod  10743  modqltm1p1mod  10745  modqsubmod  10751  modqsubmodmod  10752  modqmulmod  10758  modqmulmodr  10759  modqsubdir  10762  frecuzrdgg  10785  nninfinf  10812  seq3val  10829  seqvalcd  10830  seq3feq  10849  seq3f1olemp  10884  seqfeq4g  10900  expp1  10915  expcl2lemap  10920  expnegzap  10942  expadd  10950  expmul  10953  leexp1a  10963  resq01  11027  expnlbnd  11034  nn0ltexp2  11079  nn0opth2  11094  bcval  11119  bcval5  11133  bcpasc  11136  hashunsng  11180  sseqn  11211  hashfibclem  11214  hashfibc  11215  seq3coll  11222  iswrdiz  11239  sswrd  11241  ccatalpha  11309  ccatw2s1p1g  11341  swrdwrdsymbg  11364  swrdsb0eq  11365  ccatswrd  11370  pfxf  11382  pfxwrdsymbg  11390  wrd2ind  11423  swrdccatin2  11429  pfxccatin12lem2  11431  pfxccatin12lem3  11432  pfxccatin12  11433  pfxccat3  11434  swrdccat  11435  shftfvalg  11511  shftfval  11514  seq3shft  11531  caucvgrelemrec  11672  resqrexlemdecn  11705  sqrtmul  11728  sqrtdiv  11735  leabs  11767  absexpzap  11773  ltabs  11780  abslt  11781  absle  11782  abssubap0  11783  amgm2  11811  icodiamlt  11873  qdenre  11895  maxleim  11898  maxleastlt  11908  rexico  11914  zmaxcl  11917  minmax  11923  xrmaxleastlt  11949  xrminmax  11958  climuni  11986  cn1lem  12007  iserex  12032  iserle  12035  climserle  12038  climcau  12040  summodclem2a  12075  summodc  12077  isumss  12085  fisumss  12086  fsumadd  12100  isumadd  12125  fsum2dlemstep  12128  fsum2d  12129  fisum0diag2  12141  fsumabs  12159  isumsplit  12185  geolim  12205  geo2lim  12210  geoisum  12211  geoisumr  12212  geoisum1  12213  mertenslemub  12228  mertenslemi1  12229  mertenslem2  12230  mertensabs  12231  prodmodclem2  12271  prodmodc  12272  zproddc  12273  fprodseq  12277  fprodcl2lem  12299  fprod2dlemstep  12316  fprodle  12334  fprodmodd  12335  efcvgfsum  12361  eftlcl  12382  reeftlcl  12383  tanaddap  12433  zdvdsdc  12506  dvds2ln  12518  dvdsle  12538  divconjdvds  12543  dvdsext  12549  bitsfzo  12649  gcdsupex  12661  gcdsupcl  12662  bezoutlemmain  12702  bezoutlemaz  12707  bezoutlembi  12709  bezout  12715  gcdmultiplez  12725  dvdsmulgcd  12729  bezoutr  12736  bezoutr1  12737  lcmval  12768  lcmcllem  12772  ncoprmgcdne1b  12794  cncongr1  12808  isprm5  12847  prmdvdsexp  12853  sqrt2irr  12867  pw2dvdslemn  12870  pw2dvdseu  12873  nonsq  12912  powm2modprm  12958  pcmul  13007  pcqmul  13009  pcexp  13015  pcneg  13031  pcdvdstr  13033  pcprmpw2  13039  pcfac  13056  expnprm  13059  prmpwdvds  13061  mul4sq  13100  ballotfilem2  13153  ballotfilemfc0  13157  ballotfilemfcc  13158  ssnnctlemct  13218  infpn2  13228  isstruct2r  13244  setsfun  13268  setsfun0  13269  ismndd  13671  submnd0  13678  mhmf1o  13704  resmhm  13721  mhmco  13724  mhmima  13725  dfgrp2  13761  grprcan  13771  grplmulf1o  13808  grplactcnv  13836  pwssub  13847  mhmmnd  13854  mulgval  13860  mulgz  13888  mulgnn0dir  13890  mulgdir  13892  mulgneg2  13894  mhmmulg  13901  issubg4m  13931  nmzsubg  13948  ssnmz  13949  ghmmhmb  13992  resghm  13998  ghmpreima  14004  ghmnsgpreima  14007  ghmf1o  14013  eqgabl  14068  gsumfzconst  14079  rngpropd  14120  srglmhm  14158  srgrmhm  14159  isring  14165  ringadd2  14192  ringpropd  14203  ringlghm  14226  ringrghm  14227  oppr1g  14248  dvdsrex  14265  dvdsrtr  14268  issubrg  14389  unitrrg  14436  aprnzr  14459  opprdrng  14480  islmod  14488  islmodd  14490  lmodfopne  14523  lmodprop2d  14545  lssvacl  14562  lssvsubcl  14563  lssvscl  14572  islss3  14576  lsslss  14578  lss1d  14580  lsspropdg  14628  dflidl2rng  14678  gsumfzfsumlemm  14784  expghmap  14804  mulgghm2  14805  znval  14833  znunit  14856  znrrg  14857  psrbaglesuppg  14870  mplvalcoe  14894  neissex  15079  tgrest  15083  ssrest  15096  restopn2  15097  cnco  15135  cnss1  15140  cnss2  15141  cnptopresti  15152  uptx  15188  txrest  15190  psmetres2  15247  xmetres2  15293  xblss2ps  15318  blhalf  15322  blssexps  15343  blssex  15344  blin2  15346  blbas  15347  bdmetval  15414  metcnpi  15429  metcnpi2  15430  qtopbas  15436  tgqioo  15469  cncfss  15497  mulc1cncf  15503  cncfmptid  15511  dedekindicc  15547  ivthdec  15558  cnplimcim  15581  cnplimclemle  15582  cnplimccntop  15584  limccnp2cntop  15591  dvfgg  15602  dvcj  15623  dvrecap  15627  dvmptfsum  15639  dveflem  15640  elply2  15649  ply1termlem  15656  plymullem1  15662  eflt  15689  ptolemy  15738  cos11  15767  rpcxpmul2  15827  cxplt  15830  cxple  15831  cxplt3  15834  apcxp2  15853  rprelogbmul  15869  rprelogbdiv  15871  pellexlem3  15896  sgmval  15900  sgmval2  15901  sgmf  15903  sgmmul  15913  perfect  15918  lgsval2lem  15932  lgsdir2lem5  15954  2sqlem6  16042  umgrnloopv  16158  upgredg  16188  usgr1eop  16289  upgredginwlk  16400  wlkv0  16413  clwwlkccatlem  16444  pw1map  16818  pwtrufal  16820  nninfalllem1  16835  nninfsellemqall  16842  nnnninfex  16849  sbthom  16855  qdencn  16856  isomninnlem  16863  trirec0  16877  apdiff  16881  qdiff  16882  iswomninnlem  16883  ismkvnnlem  16886  ltlenmkv  16905