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  1060  simp2ll  1064  simp3ll  1068  rmob  3056  prneimg  3775  exmid01  4199  pwntru  4200  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  poinxp  4696  mpteqb  5607  fvmptt  5608  fcof1  5784  acexmid  5874  dftpos4  6264  tfrlem3ag  6310  tfrlem3a  6311  tfrlemi1  6333  tfrexlem  6335  tfr1onlem3ag  6338  nntr2  6504  dcdifsnid  6505  qsel  6612  ecopovsymg  6634  ecopoverg  6636  th3qlem1  6637  mapss  6691  xpmapenlem  6849  findcard2  6889  findcard2s  6890  findcard2sd  6892  unfiin  6925  f1finf1o  6946  fidcenumlemrk  6953  fidcenumlemr  6954  fidcenum  6955  sbthlemi6  6961  sbthlemi8  6963  elfi2  6971  supisolem  7007  enumct  7114  ismkvnex  7153  exmidontriimlem4  7223  netap  7253  2omotaplemap  7256  cc2lem  7265  dfplpq2  7353  dfmpq2  7354  mulpipqqs  7372  distrnqg  7386  ltexnqq  7407  subhalfnqq  7413  prarloclemarch  7417  nnnq0lem1  7445  distrnq0  7458  npsspw  7470  prarloclemlo  7493  prarloclem3  7496  prarloclemcalc  7501  genplt2i  7509  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  ltprordil  7588  ltexprlemlol  7601  ltexprlemupu  7603  addextpr  7620  recexprlemopl  7624  recexprlemdisj  7629  recexprlem1ssl  7632  aptiprleml  7638  prsrlem1  7741  recexgt0sr  7772  addcnsr  7833  mulcnsr  7834  mulcnsrec  7842  axaddcl  7863  axmulcl  7865  axmulcom  7870  rereceu  7888  ltntri  8085  cnegexlem1  8132  cnegex  8135  addsub4  8200  le2add  8401  lt2add  8402  lt2sub  8417  le2sub  8418  rereim  8543  apreim  8560  mulreim  8561  addext  8567  mulext  8571  receuap  8626  rec11ap  8667  rec11rap  8668  divdivdivap  8670  ddcanap  8683  divadddivap  8684  divsubdivap  8685  conjmulap  8686  rerecclap  8687  subrecap  8796  recgt0  8807  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  ltmul12a  8817  lemul12a  8819  lemulge11  8823  lt2mul2div  8836  ltrec  8840  lerec  8841  lt2msq  8843  ltrec1  8845  le2msq  8858  msq11  8859  ledivp1  8860  mulle0r  8901  peano5uzti  9361  eluzuzle  9536  qreccl  9642  elpq  9648  xrltso  9796  z2ge  9826  xpncan  9871  xaddge0  9878  xle2add  9879  xleaddadd  9887  ixxss1  9904  ixxss2  9905  elioc2  9936  divelunit  10002  fzass4  10062  fzrev  10084  fzonmapblen  10187  elfzodifsumelfzo  10201  ssfzo12bi  10225  rebtwn2z  10255  qbtwnxr  10258  modqid  10349  modqcyc  10359  modqaddabs  10362  modqaddmod  10363  mulqaddmodid  10364  modqadd2mod  10374  modqltm1p1mod  10376  modqsubmod  10382  modqsubmodmod  10383  modqmulmod  10389  modqmulmodr  10390  modqsubdir  10393  frecuzrdgg  10416  seq3val  10458  seqvalcd  10459  seq3feq  10472  seq3f1olemp  10502  expp1  10527  expcl2lemap  10532  expnegzap  10554  expadd  10562  expmul  10565  leexp1a  10575  expnlbnd  10645  nn0ltexp2  10689  nn0opth2  10704  bcval  10729  bcval5  10743  bcpasc  10746  hashunsng  10787  seq3coll  10822  shftfvalg  10827  shftfval  10830  seq3shft  10847  caucvgrelemrec  10988  resqrexlemdecn  11021  sqrtmul  11044  sqrtdiv  11051  leabs  11083  absexpzap  11089  ltabs  11096  abslt  11097  absle  11098  abssubap0  11099  amgm2  11127  icodiamlt  11189  qdenre  11211  maxleim  11214  maxleastlt  11224  rexico  11230  zmaxcl  11233  minmax  11238  xrmaxleastlt  11264  xrminmax  11273  climuni  11301  cn1lem  11322  iserex  11347  iserle  11350  climserle  11353  climcau  11355  summodclem2a  11389  summodc  11391  isumss  11399  fisumss  11400  fsumadd  11414  isumadd  11439  fsum2dlemstep  11442  fsum2d  11443  fisum0diag2  11455  fsumabs  11473  isumsplit  11499  geolim  11519  geo2lim  11524  geoisum  11525  geoisumr  11526  geoisum1  11527  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodcl2lem  11613  fprod2dlemstep  11630  fprodle  11648  fprodmodd  11649  efcvgfsum  11675  eftlcl  11696  reeftlcl  11697  tanaddap  11747  zdvdsdc  11819  dvds2ln  11831  dvdsle  11850  divconjdvds  11855  dvdsext  11861  gcdsupex  11958  gcdsupcl  11959  bezoutlemmain  11999  bezoutlemaz  12004  bezoutlembi  12006  bezout  12012  gcdmultiplez  12022  dvdsmulgcd  12026  bezoutr  12033  bezoutr1  12034  lcmval  12063  lcmcllem  12067  ncoprmgcdne1b  12089  cncongr1  12103  isprm5  12142  prmdvdsexp  12148  sqrt2irr  12162  pw2dvdslemn  12165  pw2dvdseu  12168  nonsq  12207  powm2modprm  12252  pcmul  12301  pcqmul  12303  pcexp  12309  pcneg  12324  pcdvdstr  12326  pcprmpw2  12332  pcfac  12348  expnprm  12351  prmpwdvds  12353  mul4sq  12392  ssnnctlemct  12447  infpn2  12457  isstruct2r  12473  setsfun  12497  setsfun0  12498  ismndd  12838  submnd0  12845  mhmf1o  12861  mhmco  12874  mhmima  12875  dfgrp2  12902  grprcan  12910  grplmulf1o  12944  grplactcnv  12972  mhmmnd  12980  mulgval  12986  mulgz  13011  mulgnn0dir  13013  mulgdir  13015  mulgneg2  13017  mhmmulg  13024  issubg4m  13053  nmzsubg  13070  ssnmz  13071  srglmhm  13176  srgrmhm  13177  isring  13183  ringadd2  13210  ringpropd  13217  oppr1g  13252  dvdsrex  13267  dvdsrtr  13270  issubrg  13342  islmod  13381  islmodd  13383  lmodfopne  13416  lmodprop2d  13438  neissex  13668  tgrest  13672  ssrest  13685  restopn2  13686  cnco  13724  cnss1  13729  cnss2  13730  cnptopresti  13741  uptx  13777  txrest  13779  psmetres2  13836  xmetres2  13882  xblss2ps  13907  blhalf  13911  blssexps  13932  blssex  13933  blin2  13935  blbas  13936  bdmetval  14003  metcnpi  14018  metcnpi2  14019  qtopbas  14025  tgqioo  14050  cncfss  14073  mulc1cncf  14079  cncfmptid  14086  dedekindicc  14114  ivthdec  14125  cnplimcim  14139  cnplimclemle  14140  cnplimccntop  14142  limccnp2cntop  14149  dvfgg  14160  dvcj  14176  dvrecap  14180  dveflem  14190  eflt  14199  ptolemy  14248  cos11  14277  cxplt  14339  cxple  14340  cxplt3  14343  apcxp2  14361  rprelogbmul  14376  rprelogbdiv  14378  lgsval2lem  14414  lgsdir2lem5  14436  2sqlem6  14470  pwtrufal  14750  nninfalllem1  14760  nninfsellemqall  14767  sbthom  14777  qdencn  14778  isomninnlem  14781  trirec0  14795  apdiff  14799  iswomninnlem  14800  ismkvnnlem  14803  ltlenmkv  14820