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  3139  ifnefals  3671  ifeqeqxdc  3673  prneimg  3883  exmid01  4316  pwntru  4317  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  poinxp  4824  mpteqb  5773  fvmptt  5774  fcof1  5962  acexmid  6057  fsuppeqg  6461  fvn0elsupp  6464  suppssdc  6473  suppssfvg  6476  dftpos4  6507  tfrlem3ag  6553  tfrlem3a  6554  tfrlemi1  6576  tfrexlem  6578  tfr1onlem3ag  6581  nntr2  6749  dcdifsnid  6750  qsel  6859  ecopovsymg  6881  ecopoverg  6883  th3qlem1  6884  mapss  6939  xpmapenlem  7115  findcard2  7159  findcard2s  7160  findcard2sd  7162  unfiin  7199  f1finf1o  7230  fidcenumlemrk  7237  fidcenumlemr  7238  fidcenum  7239  sbthlemi6  7245  sbthlemi8  7247  elfi2  7272  2omap  7282  2omapfi  7284  supisolem  7312  enumct  7419  nninfninc  7427  ismkvnex  7459  exmidontriimlem4  7544  netap  7584  2omotaplemap  7587  cc2lem  7596  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  ltexnqq  7739  subhalfnqq  7745  prarloclemarch  7749  nnnq0lem1  7777  distrnq0  7790  npsspw  7802  prarloclemlo  7825  prarloclem3  7828  prarloclemcalc  7833  genplt2i  7841  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemlol  7933  ltexprlemupu  7935  addextpr  7952  recexprlemopl  7956  recexprlemdisj  7961  recexprlem1ssl  7964  aptiprleml  7970  prsrlem1  8073  recexgt0sr  8104  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axaddcl  8195  axmulcl  8197  axmulcom  8202  rereceu  8220  mpomulf  8280  ltntri  8418  cnegexlem1  8465  cnegex  8468  addsub4  8533  le2add  8736  lt2add  8737  lt2sub  8752  le2sub  8753  rereim  8878  apreim  8895  mulreim  8896  addext  8902  mulext  8906  receuap  8963  rec11ap  9004  rec11rap  9005  divdivdivap  9007  ddcanap  9020  divadddivap  9021  divsubdivap  9022  conjmulap  9023  rerecclap  9024  subrecap  9133  recgt0  9144  prodgt0gt0  9145  prodgt0  9146  prodge0  9148  ltmul12a  9154  lemul12a  9156  lemulge11  9160  lt2mul2div  9173  ltrec  9177  lerec  9178  lt2msq  9180  ltrec1  9182  le2msq  9195  msq11  9196  ledivp1  9197  mulle0r  9238  peano5uzti  9707  eluzuzle  9883  qreccl  9995  elpq  10002  xrltso  10151  z2ge  10181  xpncan  10226  xaddge0  10233  xle2add  10234  xleaddadd  10242  ixxss1  10259  ixxss2  10260  elioc2  10291  divelunit  10357  fzass4  10420  fzrev  10443  fzonmapblen  10551  elfzodifsumelfzo  10571  ssfzo12bi  10595  rebtwn2z  10641  qbtwnxr  10644  modqid  10738  modqcyc  10748  modqaddabs  10751  modqaddmod  10752  mulqaddmodid  10753  modqadd2mod  10763  modqltm1p1mod  10765  modqsubmod  10771  modqsubmodmod  10772  modqmulmod  10778  modqmulmodr  10779  modqsubdir  10782  frecuzrdgg  10805  nninfinf  10832  seq3val  10849  seqvalcd  10850  seq3feq  10869  seq3f1olemp  10904  seqfeq4g  10920  expp1  10935  expcl2lemap  10940  expnegzap  10962  expadd  10970  expmul  10973  leexp1a  10983  resq01  11047  expnlbnd  11054  nn0ltexp2  11099  nn0opth2  11114  bcval  11139  bcval5  11153  bcpasc  11156  hashunsng  11200  sseqn  11231  hashfibclem  11234  hashfibc  11235  seq3coll  11242  iswrdiz  11259  sswrd  11261  ccatalpha  11329  ccatw2s1p1g  11361  swrdwrdsymbg  11384  swrdsb0eq  11385  ccatswrd  11390  pfxf  11402  pfxwrdsymbg  11410  wrd2ind  11443  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccatin12  11453  pfxccat3  11454  swrdccat  11455  shftfvalg  11531  shftfval  11534  seq3shft  11551  caucvgrelemrec  11692  resqrexlemdecn  11725  sqrtmul  11748  sqrtdiv  11755  leabs  11787  absexpzap  11793  ltabs  11800  abslt  11801  absle  11802  abssubap0  11803  amgm2  11831  icodiamlt  11893  qdenre  11915  maxleim  11918  maxleastlt  11928  rexico  11934  zmaxcl  11937  minmax  11943  xrmaxleastlt  11969  xrminmax  11978  climuni  12006  cn1lem  12027  iserex  12052  iserle  12055  climserle  12058  climcau  12060  summodclem2a  12095  summodc  12097  isumss  12105  fisumss  12106  fsumadd  12120  isumadd  12145  fsum2dlemstep  12148  fsum2d  12149  fisum0diag2  12161  fsumabs  12179  isumsplit  12205  geolim  12225  geo2lim  12230  geoisum  12231  geoisumr  12232  geoisum1  12233  mertenslemub  12248  mertenslemi1  12249  mertenslem2  12250  mertensabs  12251  prodmodclem2  12291  prodmodc  12292  zproddc  12293  fprodseq  12297  fprodcl2lem  12319  fprod2dlemstep  12336  fprodle  12354  fprodmodd  12355  efcvgfsum  12381  eftlcl  12402  reeftlcl  12403  tanaddap  12453  zdvdsdc  12526  dvds2ln  12538  dvdsle  12558  divconjdvds  12563  dvdsext  12569  bitsfzo  12669  gcdsupex  12681  gcdsupcl  12682  bezoutlemmain  12722  bezoutlemaz  12727  bezoutlembi  12729  bezout  12735  gcdmultiplez  12745  dvdsmulgcd  12749  bezoutr  12756  bezoutr1  12757  lcmval  12788  lcmcllem  12792  ncoprmgcdne1b  12814  cncongr1  12828  isprm5  12867  prmdvdsexp  12873  sqrt2irr  12887  pw2dvdslemn  12890  pw2dvdseu  12893  nonsq  12932  powm2modprm  12978  pcmul  13027  pcqmul  13029  pcexp  13035  pcneg  13051  pcdvdstr  13053  pcprmpw2  13059  pcfac  13076  expnprm  13079  prmpwdvds  13081  mul4sq  13120  ballotfilem2  13175  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemsima  13206  ssnnctlemct  13284  infpn2  13294  isstruct2r  13310  setsfun  13334  setsfun0  13335  ismndd  13701  submnd0  13708  mhmf1o  13728  resmhm  13745  mhmco  13748  mhmima  13749  dfgrp2  13785  grprcan  13795  grplmulf1o  13832  grplactcnv  13860  mhmmnd  13872  mulgval  13878  mulgz  13906  mulgnn0dir  13908  mulgdir  13910  mulgneg2  13912  mhmmulg  13919  issubg4m  13949  nmzsubg  13966  ssnmz  13967  ghmmhmb  14010  resghm  14016  ghmpreima  14022  ghmnsgpreima  14025  ghmf1o  14031  eqgabl  14086  gsumfzconst  14097  pwssub  14161  rngpropd  14197  srglmhm  14239  srgrmhm  14240  isring  14246  ringadd2  14273  ringpropd  14284  ringlghm  14307  ringrghm  14308  oppr1g  14329  dvdsrex  14346  dvdsrtr  14349  issubrg  14470  unitrrg  14517  aprnzr  14540  opprdrng  14561  islmod  14568  islmodd  14570  lmodfopne  14603  lmodprop2d  14625  lssvacl  14642  lssvsubcl  14643  lssvscl  14652  islss3  14656  lsslss  14658  lss1d  14660  lsspropdg  14708  dflidl2rng  14758  gsumfzfsumlemm  14864  expghmap  14884  mulgghm2  14885  znval  14913  znunit  14936  znrrg  14937  psrbaglesuppg  14950  mplvalcoe  14974  neissex  15159  tgrest  15163  ssrest  15176  restopn2  15177  cnco  15215  cnss1  15220  cnss2  15221  cnptopresti  15232  uptx  15268  txrest  15270  psmetres2  15327  xmetres2  15373  xblss2ps  15398  blhalf  15402  blssexps  15423  blssex  15424  blin2  15426  blbas  15427  bdmetval  15494  metcnpi  15509  metcnpi2  15510  qtopbas  15516  tgqioo  15549  cncfss  15577  mulc1cncf  15583  cncfmptid  15591  dedekindicc  15627  ivthdec  15638  cnplimcim  15661  cnplimclemle  15662  cnplimccntop  15664  limccnp2cntop  15671  dvfgg  15682  dvcj  15703  dvrecap  15707  dvmptfsum  15719  dveflem  15720  elply2  15729  ply1termlem  15736  plymullem1  15742  eflt  15769  ptolemy  15818  cos11  15847  rpcxpmul2  15907  cxplt  15910  cxple  15911  cxplt3  15914  apcxp2  15933  rprelogbmul  15949  rprelogbdiv  15951  pellexlem3  15976  sgmval  15980  sgmval2  15981  sgmf  15983  sgmmul  15993  perfect  15998  lgsval2lem  16012  lgsdir2lem5  16034  2sqlem6  16122  umgrnloopv  16238  upgredg  16268  usgr1eop  16369  upgredginwlk  16480  wlkv0  16493  clwwlkccatlem  16524  pw1map  16908  pwtrufal  16910  nninfalllem1  16925  nninfsellemqall  16932  nnnninfex  16939  sbthom  16945  qdencn  16946  isomninnlem  16953  trirec0  16967  apdiff  16971  qdiff  16972  iswomninnlem  16973  ismkvnnlem  16976  ltlenmkv  16995