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  3122  ifnefals  3647  prneimg  3852  exmid01  4282  pwntru  4283  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  poinxp  4788  mpteqb  5727  fvmptt  5728  fcof1  5913  acexmid  6006  dftpos4  6415  tfrlem3ag  6461  tfrlem3a  6462  tfrlemi1  6484  tfrexlem  6486  tfr1onlem3ag  6489  nntr2  6657  dcdifsnid  6658  qsel  6767  ecopovsymg  6789  ecopoverg  6791  th3qlem1  6792  mapss  6846  xpmapenlem  7018  findcard2  7059  findcard2s  7060  findcard2sd  7062  unfiin  7096  f1finf1o  7122  fidcenumlemrk  7129  fidcenumlemr  7130  fidcenum  7131  sbthlemi6  7137  sbthlemi8  7139  elfi2  7147  supisolem  7183  enumct  7290  nninfninc  7298  ismkvnex  7330  exmidontriimlem4  7414  netap  7448  2omotaplemap  7451  cc2lem  7460  dfplpq2  7549  dfmpq2  7550  mulpipqqs  7568  distrnqg  7582  ltexnqq  7603  subhalfnqq  7609  prarloclemarch  7613  nnnq0lem1  7641  distrnq0  7654  npsspw  7666  prarloclemlo  7689  prarloclem3  7692  prarloclemcalc  7697  genplt2i  7705  distrlem1prl  7777  distrlem1pru  7778  distrlem4prl  7779  distrlem4pru  7780  ltprordil  7784  ltexprlemlol  7797  ltexprlemupu  7799  addextpr  7816  recexprlemopl  7820  recexprlemdisj  7825  recexprlem1ssl  7828  aptiprleml  7834  prsrlem1  7937  recexgt0sr  7968  addcnsr  8029  mulcnsr  8030  mulcnsrec  8038  axaddcl  8059  axmulcl  8061  axmulcom  8066  rereceu  8084  mpomulf  8144  ltntri  8282  cnegexlem1  8329  cnegex  8332  addsub4  8397  le2add  8599  lt2add  8600  lt2sub  8615  le2sub  8616  rereim  8741  apreim  8758  mulreim  8759  addext  8765  mulext  8769  receuap  8824  rec11ap  8865  rec11rap  8866  divdivdivap  8868  ddcanap  8881  divadddivap  8882  divsubdivap  8883  conjmulap  8884  rerecclap  8885  subrecap  8994  recgt0  9005  prodgt0gt0  9006  prodgt0  9007  prodge0  9009  ltmul12a  9015  lemul12a  9017  lemulge11  9021  lt2mul2div  9034  ltrec  9038  lerec  9039  lt2msq  9041  ltrec1  9043  le2msq  9056  msq11  9057  ledivp1  9058  mulle0r  9099  peano5uzti  9563  eluzuzle  9738  qreccl  9845  elpq  9852  xrltso  10000  z2ge  10030  xpncan  10075  xaddge0  10082  xle2add  10083  xleaddadd  10091  ixxss1  10108  ixxss2  10109  elioc2  10140  divelunit  10206  fzass4  10266  fzrev  10288  fzonmapblen  10395  elfzodifsumelfzo  10415  ssfzo12bi  10439  rebtwn2z  10482  qbtwnxr  10485  modqid  10579  modqcyc  10589  modqaddabs  10592  modqaddmod  10593  mulqaddmodid  10594  modqadd2mod  10604  modqltm1p1mod  10606  modqsubmod  10612  modqsubmodmod  10613  modqmulmod  10619  modqmulmodr  10620  modqsubdir  10623  frecuzrdgg  10646  nninfinf  10673  seq3val  10690  seqvalcd  10691  seq3feq  10710  seq3f1olemp  10745  seqfeq4g  10761  expp1  10776  expcl2lemap  10781  expnegzap  10803  expadd  10811  expmul  10814  leexp1a  10824  expnlbnd  10894  nn0ltexp2  10939  nn0opth2  10954  bcval  10979  bcval5  10993  bcpasc  10996  hashunsng  11037  seq3coll  11072  iswrdiz  11086  sswrd  11088  swrdwrdsymbg  11204  swrdsb0eq  11205  ccatswrd  11210  pfxf  11222  pfxwrdsymbg  11230  wrd2ind  11263  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccatin12  11273  pfxccat3  11274  swrdccat  11275  shftfvalg  11337  shftfval  11340  seq3shft  11357  caucvgrelemrec  11498  resqrexlemdecn  11531  sqrtmul  11554  sqrtdiv  11561  leabs  11593  absexpzap  11599  ltabs  11606  abslt  11607  absle  11608  abssubap0  11609  amgm2  11637  icodiamlt  11699  qdenre  11721  maxleim  11724  maxleastlt  11734  rexico  11740  zmaxcl  11743  minmax  11749  xrmaxleastlt  11775  xrminmax  11784  climuni  11812  cn1lem  11833  iserex  11858  iserle  11861  climserle  11864  climcau  11866  summodclem2a  11900  summodc  11902  isumss  11910  fisumss  11911  fsumadd  11925  isumadd  11950  fsum2dlemstep  11953  fsum2d  11954  fisum0diag2  11966  fsumabs  11984  isumsplit  12010  geolim  12030  geo2lim  12035  geoisum  12036  geoisumr  12037  geoisum1  12038  mertenslemub  12053  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  prodmodclem2  12096  prodmodc  12097  zproddc  12098  fprodseq  12102  fprodcl2lem  12124  fprod2dlemstep  12141  fprodle  12159  fprodmodd  12160  efcvgfsum  12186  eftlcl  12207  reeftlcl  12208  tanaddap  12258  zdvdsdc  12331  dvds2ln  12343  dvdsle  12363  divconjdvds  12368  dvdsext  12374  bitsfzo  12474  gcdsupex  12486  gcdsupcl  12487  bezoutlemmain  12527  bezoutlemaz  12532  bezoutlembi  12534  bezout  12540  gcdmultiplez  12550  dvdsmulgcd  12554  bezoutr  12561  bezoutr1  12562  lcmval  12593  lcmcllem  12597  ncoprmgcdne1b  12619  cncongr1  12633  isprm5  12672  prmdvdsexp  12678  sqrt2irr  12692  pw2dvdslemn  12695  pw2dvdseu  12698  nonsq  12737  powm2modprm  12783  pcmul  12832  pcqmul  12834  pcexp  12840  pcneg  12856  pcdvdstr  12858  pcprmpw2  12864  pcfac  12881  expnprm  12884  prmpwdvds  12886  mul4sq  12925  ssnnctlemct  13025  infpn2  13035  isstruct2r  13051  setsfun  13075  setsfun0  13076  ismndd  13478  submnd0  13485  mhmf1o  13511  resmhm  13528  mhmco  13531  mhmima  13532  dfgrp2  13568  grprcan  13578  grplmulf1o  13615  grplactcnv  13643  pwssub  13654  mhmmnd  13661  mulgval  13667  mulgz  13695  mulgnn0dir  13697  mulgdir  13699  mulgneg2  13701  mhmmulg  13708  issubg4m  13738  nmzsubg  13755  ssnmz  13756  ghmmhmb  13799  resghm  13805  ghmpreima  13811  ghmnsgpreima  13814  ghmf1o  13820  eqgabl  13875  gsumfzconst  13886  rngpropd  13926  srglmhm  13964  srgrmhm  13965  isring  13971  ringadd2  13998  ringpropd  14009  ringlghm  14032  ringrghm  14033  oppr1g  14053  dvdsrex  14070  dvdsrtr  14073  issubrg  14193  unitrrg  14239  islmod  14263  islmodd  14265  lmodfopne  14298  lmodprop2d  14320  lssvacl  14337  lssvsubcl  14338  lssvscl  14347  islss3  14351  lsslss  14353  lss1d  14355  lsspropdg  14403  dflidl2rng  14453  gsumfzfsumlemm  14559  expghmap  14579  mulgghm2  14580  znval  14608  znunit  14631  znrrg  14632  psrbaglesuppg  14644  mplvalcoe  14662  neissex  14847  tgrest  14851  ssrest  14864  restopn2  14865  cnco  14903  cnss1  14908  cnss2  14909  cnptopresti  14920  uptx  14956  txrest  14958  psmetres2  15015  xmetres2  15061  xblss2ps  15086  blhalf  15090  blssexps  15111  blssex  15112  blin2  15114  blbas  15115  bdmetval  15182  metcnpi  15197  metcnpi2  15198  qtopbas  15204  tgqioo  15237  cncfss  15265  mulc1cncf  15271  cncfmptid  15279  dedekindicc  15315  ivthdec  15326  cnplimcim  15349  cnplimclemle  15350  cnplimccntop  15352  limccnp2cntop  15359  dvfgg  15370  dvcj  15391  dvrecap  15395  dvmptfsum  15407  dveflem  15408  elply2  15417  ply1termlem  15424  plymullem1  15430  eflt  15457  ptolemy  15506  cos11  15535  rpcxpmul2  15595  cxplt  15598  cxple  15599  cxplt3  15602  apcxp2  15621  rprelogbmul  15637  rprelogbdiv  15639  sgmval  15665  sgmval2  15666  sgmf  15668  sgmmul  15678  perfect  15683  lgsval2lem  15697  lgsdir2lem5  15719  2sqlem6  15807  umgrnloopv  15922  upgredg  15950  upgredginwlk  16077  wlkv0  16090  2omap  16388  pw1map  16390  pwtrufal  16392  nninfalllem1  16404  nninfsellemqall  16411  nnnninfex  16418  sbthom  16424  qdencn  16425  isomninnlem  16428  trirec0  16442  apdiff  16446  iswomninnlem  16447  ismkvnnlem  16450  ltlenmkv  16468