Theorem simpll 495

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 471	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  simp1ll  1001  simp2ll  1005  simp3ll  1009  rmob  2906  prneimg  3566  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  poinxp  4427  mpteqb  5282  fvmptt  5283  fcof1  5443  acexmid  5531  grprinvlem  5715  dftpos4  5901  tfrlem3ag  5947  tfrlem3a  5948  tfrlemi1  5969  tfrexlem  5971  nndifsnid  6103  qsel  6206  ecopovsymg  6228  ecopoverg  6230  th3qlem1  6231  fidifsnid  6356  findcard2  6373  findcard2s  6374  findcard2sd  6376  supisolem  6421  dfplpq2  6544  dfmpq2  6545  mulpipqqs  6563  distrnqg  6577  ltexnqq  6598  subhalfnqq  6604  prarloclemarch  6608  nnnq0lem1  6636  distrnq0  6649  npsspw  6661  prarloclemlo  6684  prarloclem3  6687  prarloclemcalc  6692  genplt2i  6700  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  ltexprlemlol  6792  ltexprlemupu  6794  addextpr  6811  recexprlemopl  6815  recexprlemdisj  6820  recexprlem1ssl  6823  aptiprleml  6829  prsrlem1  6919  recexgt0sr  6950  addcnsr  7002  mulcnsr  7003  mulcnsrec  7011  axaddcl  7032  axmulcl  7034  axmulcom  7037  rereceu  7055  cnegexlem1  7283  cnegex  7286  addsub4  7351  le2add  7548  lt2add  7549  lt2sub  7564  le2sub  7565  rereim  7686  apreim  7703  mulreim  7704  addext  7710  mulext  7714  receuap  7759  rec11ap  7798  rec11rap  7799  divdivdivap  7801  ddcanap  7814  divadddivap  7815  divsubdivap  7816  conjmulap  7817  rerecclap  7818  recgt0  7928  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  ltmul12a  7938  lemul12a  7940  lemulge11  7944  lt2mul2div  7957  ltrec  7961  lerec  7962  lt2msq  7964  ltrec1  7966  le2msq  7979  msq11  7980  ledivp1  7981  mulle0r  8022  peano5uzti  8455  eluzuzle  8627  qreccl  8727  xrltso  8871  z2ge  8893  ixxss1  8927  ixxss2  8928  elioc2  8959  divelunit  9024  fzass4  9080  fzrev  9101  fzonmapblen  9196  elfzodifsumelfzo  9210  ssfzo12bi  9234  qbtwnzlemstep  9257  qbtwnzlemex  9259  rebtwn2z  9263  qbtwnxr  9266  modqid  9351  modqcyc  9361  modqaddabs  9364  modqaddmod  9365  mulqaddmodid  9366  modqadd2mod  9376  modqltm1p1mod  9378  modqsubmod  9384  modqsubmodmod  9385  modqmulmod  9391  modqmulmodr  9392  modqsubdir  9395  expivallem  9477  expp1  9483  expcl2lemap  9488  expnegzap  9510  expadd  9518  expmul  9521  leexp1a  9531  expnlbnd  9597  nn0opth2  9651  bcval  9676  ibcval5  9690  bcpasc  9693  shftfvalg  9706  shftfval  9709  caucvgrelemrec  9865  resqrexlemdecn  9898  sqrtmul  9921  sqrtdiv  9928  leabs  9960  absexpzap  9966  ltabs  9973  abslt  9974  absle  9975  abssubap0  9976  amgm2  10004  icodiamlt  10066  qdenre  10088  maxleim  10091  maxleastlt  10101  rexico  10107  minmax  10112  climuni  10132  cn1lem  10152  iiserex  10177  iserile  10180  climcau  10184  zdvdsdc  10216  dvds2ln  10228  dvdsle  10244  divconjdvds  10249  dvdsext  10255  gcdsupex  10349  gcdsupcl  10350  bezoutlemmain  10387  bezoutlemaz  10392  bezoutlembi  10394  bezout  10400  gcdmultiplez  10410  dvdsmulgcd  10414  bezoutr  10421  bezoutr1  10422  lcmval  10445  lcmcllem  10449  ncoprmgcdne1b  10471  cncongr1  10485  prmdvdsexp  10527  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseu  10546  qdencn  10785