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  1062  simp2ll  1066  simp3ll  1070  rmob  3082  ifnefals  3604  prneimg  3805  exmid01  4232  pwntru  4233  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  poinxp  4733  mpteqb  5655  fvmptt  5656  fcof1  5833  acexmid  5924  dftpos4  6330  tfrlem3ag  6376  tfrlem3a  6377  tfrlemi1  6399  tfrexlem  6401  tfr1onlem3ag  6404  nntr2  6570  dcdifsnid  6571  qsel  6680  ecopovsymg  6702  ecopoverg  6704  th3qlem1  6705  mapss  6759  xpmapenlem  6919  findcard2  6959  findcard2s  6960  findcard2sd  6962  unfiin  6996  f1finf1o  7022  fidcenumlemrk  7029  fidcenumlemr  7030  fidcenum  7031  sbthlemi6  7037  sbthlemi8  7039  elfi2  7047  supisolem  7083  enumct  7190  nninfninc  7198  ismkvnex  7230  exmidontriimlem4  7307  netap  7337  2omotaplemap  7340  cc2lem  7349  dfplpq2  7438  dfmpq2  7439  mulpipqqs  7457  distrnqg  7471  ltexnqq  7492  subhalfnqq  7498  prarloclemarch  7502  nnnq0lem1  7530  distrnq0  7543  npsspw  7555  prarloclemlo  7578  prarloclem3  7581  prarloclemcalc  7586  genplt2i  7594  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  ltprordil  7673  ltexprlemlol  7686  ltexprlemupu  7688  addextpr  7705  recexprlemopl  7709  recexprlemdisj  7714  recexprlem1ssl  7717  aptiprleml  7723  prsrlem1  7826  recexgt0sr  7857  addcnsr  7918  mulcnsr  7919  mulcnsrec  7927  axaddcl  7948  axmulcl  7950  axmulcom  7955  rereceu  7973  mpomulf  8033  ltntri  8171  cnegexlem1  8218  cnegex  8221  addsub4  8286  le2add  8488  lt2add  8489  lt2sub  8504  le2sub  8505  rereim  8630  apreim  8647  mulreim  8648  addext  8654  mulext  8658  receuap  8713  rec11ap  8754  rec11rap  8755  divdivdivap  8757  ddcanap  8770  divadddivap  8771  divsubdivap  8772  conjmulap  8773  rerecclap  8774  subrecap  8883  recgt0  8894  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  ltmul12a  8904  lemul12a  8906  lemulge11  8910  lt2mul2div  8923  ltrec  8927  lerec  8928  lt2msq  8930  ltrec1  8932  le2msq  8945  msq11  8946  ledivp1  8947  mulle0r  8988  peano5uzti  9451  eluzuzle  9626  qreccl  9733  elpq  9740  xrltso  9888  z2ge  9918  xpncan  9963  xaddge0  9970  xle2add  9971  xleaddadd  9979  ixxss1  9996  ixxss2  9997  elioc2  10028  divelunit  10094  fzass4  10154  fzrev  10176  fzonmapblen  10280  elfzodifsumelfzo  10294  ssfzo12bi  10318  rebtwn2z  10361  qbtwnxr  10364  modqid  10458  modqcyc  10468  modqaddabs  10471  modqaddmod  10472  mulqaddmodid  10473  modqadd2mod  10483  modqltm1p1mod  10485  modqsubmod  10491  modqsubmodmod  10492  modqmulmod  10498  modqmulmodr  10499  modqsubdir  10502  frecuzrdgg  10525  nninfinf  10552  seq3val  10569  seqvalcd  10570  seq3feq  10589  seq3f1olemp  10624  seqfeq4g  10640  expp1  10655  expcl2lemap  10660  expnegzap  10682  expadd  10690  expmul  10693  leexp1a  10703  expnlbnd  10773  nn0ltexp2  10818  nn0opth2  10833  bcval  10858  bcval5  10872  bcpasc  10875  hashunsng  10916  seq3coll  10951  iswrdiz  10959  sswrd  10961  shftfvalg  11000  shftfval  11003  seq3shft  11020  caucvgrelemrec  11161  resqrexlemdecn  11194  sqrtmul  11217  sqrtdiv  11224  leabs  11256  absexpzap  11262  ltabs  11269  abslt  11270  absle  11271  abssubap0  11272  amgm2  11300  icodiamlt  11362  qdenre  11384  maxleim  11387  maxleastlt  11397  rexico  11403  zmaxcl  11406  minmax  11412  xrmaxleastlt  11438  xrminmax  11447  climuni  11475  cn1lem  11496  iserex  11521  iserle  11524  climserle  11527  climcau  11529  summodclem2a  11563  summodc  11565  isumss  11573  fisumss  11574  fsumadd  11588  isumadd  11613  fsum2dlemstep  11616  fsum2d  11617  fisum0diag2  11629  fsumabs  11647  isumsplit  11673  geolim  11693  geo2lim  11698  geoisum  11699  geoisumr  11700  geoisum1  11701  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodcl2lem  11787  fprod2dlemstep  11804  fprodle  11822  fprodmodd  11823  efcvgfsum  11849  eftlcl  11870  reeftlcl  11871  tanaddap  11921  zdvdsdc  11994  dvds2ln  12006  dvdsle  12026  divconjdvds  12031  dvdsext  12037  bitsfzo  12137  gcdsupex  12149  gcdsupcl  12150  bezoutlemmain  12190  bezoutlemaz  12195  bezoutlembi  12197  bezout  12203  gcdmultiplez  12213  dvdsmulgcd  12217  bezoutr  12224  bezoutr1  12225  lcmval  12256  lcmcllem  12260  ncoprmgcdne1b  12282  cncongr1  12296  isprm5  12335  prmdvdsexp  12341  sqrt2irr  12355  pw2dvdslemn  12358  pw2dvdseu  12361  nonsq  12400  powm2modprm  12446  pcmul  12495  pcqmul  12497  pcexp  12503  pcneg  12519  pcdvdstr  12521  pcprmpw2  12527  pcfac  12544  expnprm  12547  prmpwdvds  12549  mul4sq  12588  ssnnctlemct  12688  infpn2  12698  isstruct2r  12714  setsfun  12738  setsfun0  12739  ismndd  13139  submnd0  13146  mhmf1o  13172  resmhm  13189  mhmco  13192  mhmima  13193  dfgrp2  13229  grprcan  13239  grplmulf1o  13276  grplactcnv  13304  pwssub  13315  mhmmnd  13322  mulgval  13328  mulgz  13356  mulgnn0dir  13358  mulgdir  13360  mulgneg2  13362  mhmmulg  13369  issubg4m  13399  nmzsubg  13416  ssnmz  13417  ghmmhmb  13460  resghm  13466  ghmpreima  13472  ghmnsgpreima  13475  ghmf1o  13481  eqgabl  13536  gsumfzconst  13547  rngpropd  13587  srglmhm  13625  srgrmhm  13626  isring  13632  ringadd2  13659  ringpropd  13670  ringlghm  13693  ringrghm  13694  oppr1g  13714  dvdsrex  13730  dvdsrtr  13733  issubrg  13853  unitrrg  13899  islmod  13923  islmodd  13925  lmodfopne  13958  lmodprop2d  13980  lssvacl  13997  lssvsubcl  13998  lssvscl  14007  islss3  14011  lsslss  14013  lss1d  14015  lsspropdg  14063  dflidl2rng  14113  gsumfzfsumlemm  14219  expghmap  14239  mulgghm2  14240  znval  14268  znunit  14291  znrrg  14292  psrbaglesuppg  14302  neissex  14485  tgrest  14489  ssrest  14502  restopn2  14503  cnco  14541  cnss1  14546  cnss2  14547  cnptopresti  14558  uptx  14594  txrest  14596  psmetres2  14653  xmetres2  14699  xblss2ps  14724  blhalf  14728  blssexps  14749  blssex  14750  blin2  14752  blbas  14753  bdmetval  14820  metcnpi  14835  metcnpi2  14836  qtopbas  14842  tgqioo  14875  cncfss  14903  mulc1cncf  14909  cncfmptid  14917  dedekindicc  14953  ivthdec  14964  cnplimcim  14987  cnplimclemle  14988  cnplimccntop  14990  limccnp2cntop  14997  dvfgg  15008  dvcj  15029  dvrecap  15033  dvmptfsum  15045  dveflem  15046  elply2  15055  ply1termlem  15062  plymullem1  15068  eflt  15095  ptolemy  15144  cos11  15173  rpcxpmul2  15233  cxplt  15236  cxple  15237  cxplt3  15240  apcxp2  15259  rprelogbmul  15275  rprelogbdiv  15277  sgmval  15303  sgmval2  15304  sgmf  15306  sgmmul  15316  perfect  15321  lgsval2lem  15335  lgsdir2lem5  15357  2sqlem6  15445  2omap  15726  pwtrufal  15728  nninfalllem1  15739  nninfsellemqall  15746  sbthom  15757  qdencn  15758  isomninnlem  15761  trirec0  15775  apdiff  15779  iswomninnlem  15780  ismkvnnlem  15783  ltlenmkv  15801