Theorem simprl 529

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprl	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad2antrl 490	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:  simp1rl  1067  simp2rl  1071  simp3rl  1075  rmob  3102  elpr2elpr  3833  disjiun  4057  reg3exmidlemwe  4648  0xp  4776  imainss  5120  iotam  5286  fvmptt  5699  fcof1o  5886  isotr  5913  riota5f  5954  ovmpodf  6107  unielxp  6290  fnmpoovd  6331  1stconst  6337  2ndconst  6338  cnvf1olem  6340  tfrlemi14d  6449  tfrexlem  6450  tfr1onlemres  6465  tfrcllemres  6478  tfrcldm  6479  frecabcl  6515  nnaordi  6624  swoer  6678  qliftfun  6734  ecopovsymg  6751  th3qlem1  6754  pw2f1odclem  6963  mapen  6975  mapxpen  6977  fidifsnen  7000  fisbth  7013  findcard2d  7021  findcard2sd  7022  diffisn  7023  diffifi  7024  ac6sfi  7028  fimax2gtri  7031  fientri3  7045  nnwetri  7046  unsnfi  7049  unsnfidcex  7050  unsnfidcel  7051  fisseneq  7064  fidcenumlemrk  7089  fidcenumlemr  7090  isbth  7102  ordiso2  7170  difinfsnlem  7234  difinfinf  7236  ctmlemr  7243  ctssdccl  7246  fodjum  7281  fodju0  7282  omniwomnimkv  7302  exmidfodomrlemrALT  7349  netap  7408  exmidmotap  7415  cc1  7419  cc2lem  7420  cc3  7422  cc4f  7423  cc4n  7425  dfplpq2  7509  dfmpq2  7510  mulpipqqs  7528  distrnqg  7542  ltexnqq  7563  subhalfnqq  7569  distrnq0  7614  prarloclemup  7650  prarloclem3  7652  prarloc  7658  genplt2i  7665  nqprl  7706  nqpru  7707  prmuloc  7721  mullocpr  7726  distrlem4prl  7739  distrlem4pru  7740  ltaddpr  7752  ltexprlemopl  7756  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemrl  7765  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  ltaprlem  7773  ltaprg  7774  prplnqu  7775  addextpr  7776  recexprlemdisj  7785  recexprlemloc  7786  recexprlem1ssl  7788  aptiprleml  7794  aptiprlemu  7795  ltmprr  7797  archpr  7798  cauappcvgprlemopl  7801  cauappcvgprlemopu  7803  cauappcvgprlemdisj  7806  cauappcvgprlemloc  7807  cauappcvgprlem1  7814  cauappcvgprlem2  7815  cauappcvgprlemlim  7816  caucvgprlemnkj  7821  caucvgprlemopl  7824  caucvgprlemopu  7826  caucvgprlemdisj  7829  caucvgprlemloc  7830  caucvgprlem2  7835  caucvgprprlemnkltj  7844  caucvgprprlemnkeqj  7845  caucvgprprlemnjltk  7846  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemopu  7854  caucvgprprlemdisj  7857  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  caucvgprprlemaddq  7863  caucvgprprlem2  7865  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemex  7877  suplocexprlemub  7878  suplocexprlemlub  7879  recexgt0sr  7928  mulgt0sr  7933  prsrriota  7943  caucvgsrlemoffres  7955  suplocsrlem  7963  cnm  7987  addcnsr  7989  mulcnsr  7990  mulcnsrec  7998  axaddcl  8019  axmulcl  8021  axmulcom  8026  rereceu  8044  recriota  8045  axcaucvglemres  8054  axpre-suploclemres  8056  lelttr  8203  ltletr  8204  readdcan  8254  addcan  8294  addcan2  8295  addsub4  8357  ltadd2  8534  le2add  8559  lt2add  8560  lt2sub  8575  le2sub  8576  eqord1  8598  rimul  8700  rereim  8701  ltmul1  8707  apreim  8718  mulreim  8719  apcotr  8722  apadd1  8723  addext  8725  apneg  8726  mulext1  8727  mulext  8729  ltleap  8747  aprcl  8761  mulap0  8769  mulcanapd  8776  receuap  8784  recapb  8786  rec11ap  8825  rec11rap  8826  divdivdivap  8828  ddcanap  8841  divadddivap  8842  conjmulap  8844  subrecap  8954  prodgt0gt0  8966  prodge0  8969  ltmul12a  8975  lemulge11  8981  lt2mul2div  8994  ltrec  8998  lerec  8999  lt2msq  9001  lerec2  9004  le2msq  9016  msq11  9017  ledivp1  9018  mulle0r  9059  suprzclex  9513  peano5uzti  9523  supinfneg  9758  infsupneg  9759  qapne  9802  xrlelttr  9970  xrltletr  9971  xrre  9984  xaddge0  10042  xle2add  10043  xlt2add  10044  divelunit  10166  fzass4  10226  fzocatel  10372  zsupcllemstep  10416  zssinfcl  10419  suprzubdc  10423  zsupssdc  10425  suprzcl2dc  10426  exbtwnzlemex  10436  rebtwn2z  10441  qbtwnre  10443  modqid  10538  modqcyc  10548  modqaddabs  10551  modqaddmod  10552  mulqaddmodid  10553  modqadd2mod  10563  modqltm1p1mod  10565  modqsubmod  10571  modqsubmodmod  10572  modqmulmod  10578  modqmulmodr  10579  modqaddmulmod  10580  modqsubdir  10582  frec2uzisod  10596  iseqovex  10647  seqvalcd  10650  seq1g  10652  seqf  10653  seqovcd  10656  seqm1g  10663  seq3fveq2  10664  seq3shft2  10670  seqshft2g  10671  monoord  10674  seq3split  10677  seqsplitg  10678  iseqf1olemnab  10690  seqf1oglem1  10708  seqf1og  10710  seq3id2  10715  seqhomog  10719  seq3distr  10721  expcl2lemap  10740  expnegzap  10762  ltexp2a  10780  le2sq2  10804  nn0ltexp2  10898  nn0opth2  10913  bcval5  10952  hashcl  10970  hashen  10973  fihashdom  10992  hashunlem  10993  hashun  10994  fimaxq  11016  zfz1isolem1  11029  zfz1iso  11030  lencl  11042  sswrd  11047  fstwrdne0  11077  lswlgt0cl  11090  swrdval  11146  wrdind  11220  wrd2ind  11221  swrdccatfn  11222  swrdccatin1  11223  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccatin12  11231  pfxccat3a  11236  reuccatpfxs1  11245  cvg1nlemres  11462  cvg1n  11463  recvguniq  11472  resqrexlemp1rp  11483  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemex  11502  sqrtmul  11512  sqrtsq  11521  absexpzap  11557  absle  11566  abs3lem  11588  amgm2  11595  maxleastlt  11692  maxltsup  11695  fimaxre2  11704  xrmaxleastlt  11733  xrmaxltsup  11735  xrmaxaddlem  11737  climcn2  11786  addcn2  11787  mulcn2  11789  reccn2ap  11790  climcau  11824  summodclem2  11859  summodc  11860  fsumf1o  11867  fisumss  11869  fsum3cvg3  11873  fsumcl2lem  11875  fsumadd  11883  fsum2dlemstep  11911  mptfzshft  11919  fsumrev  11920  fsummulc2  11925  modfsummod  11935  fsumrelem  11948  binom  11961  cvgratnn  12008  mertenslemub  12011  prodmodc  12055  zproddc  12056  fprodf1o  12065  fprodssdc  12067  fprodmul  12068  fprodrev  12096  fprod2dlemstep  12099  efcllem  12136  tanaddaplem  12215  dvdsval2  12267  moddvds  12276  dvdsabseq  12324  dvdsflip  12328  oexpneg  12354  fldivndvdslt  12414  bitsfi  12434  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemeu  12494  dfgcd3  12497  bezout  12498  dvdsmulgcd  12512  bezoutr  12519  nninfctlemfo  12527  ialgrlem1st  12530  lcmgcdlem  12565  coprmdvds2  12581  qredeu  12585  rpdvds  12587  isprm5lem  12629  isprm6  12635  pw2dvdslemn  12653  nonsq  12695  crth  12712  eulerthlemh  12719  pclemdc  12777  pcprendvds2  12780  pceu  12784  pcval  12785  pczpre  12786  pcmul  12790  pcqmul  12792  pcqcl  12795  pcid  12813  pcneg  12814  pcgcd1  12817  pc2dvds  12819  pcprmpw2  12822  difsqpwdvds  12827  pcmpt  12832  pockthg  12846  1arith  12856  mul4sq  12883  4sqexercise2  12888  ennnfonelemg  12940  ennnfonelemex  12951  ennnfonelemrnh  12953  ennnfonelemrn  12956  ennnfonelemdm  12957  ennnfonelemnn0  12959  ennnfonelemim  12961  ennnfone  12962  ctinfomlemom  12964  ctinf  12967  ctiunctlemfo  12976  nninfdclemcl  12985  nninfdclemf  12986  nninfdclemp1  12987  unbendc  12991  isstruct2r  13009  setscom  13038  qusval  13322  ercpbl  13330  opifismgmdc  13370  grpinvalem  13384  grprida  13386  igsumvalx  13388  gsumfzval  13390  gsumpropd2  13392  gsumval2  13396  sgrppropd  13412  prdssgrpd  13414  mndpropd  13439  issubmnd  13441  submnd0  13443  prdsmndd  13447  mhmf1o  13469  0mhm  13485  resmhm  13486  mhmco  13489  mhmima  13490  mhmeql  13491  gsumwsubmcl  13495  gsumfzcl  13498  grppropd  13516  grpinvid1  13551  grpinvid2  13552  grplcan  13561  grplmulf1o  13573  grpnpncan0  13595  dfgrp3mlem  13597  grplactcnv  13601  pwssub  13612  mulgval  13625  mulgfng  13627  mulg1  13632  mulgnnp1  13633  mulgneg  13643  mulgnndir  13654  mulgdirlem  13656  mulgnn0ass  13661  mulgass  13662  subgmulg  13691  issubg4m  13696  subgintm  13701  0nsg  13717  eqgcpbl  13731  ghmmulg  13759  ghmpreima  13769  ghmeql  13770  ghmnsgima  13771  ghmnsgpreima  13772  ghmf1  13776  ghmf1o  13778  conjghm  13779  conjnmzb  13783  qusghm  13785  ablpncan3  13820  invghm  13832  eqgabl  13833  qusecsub  13834  gsumfzreidx  13840  gsumfzsubmcl  13841  gsumfzmptfidmadd  13842  gsumfzmhm  13846  imasrng  13885  qusrng  13887  srglmhm  13922  srgrmhm  13923  ringpropd  13967  ringlghm  13990  ringrghm  13991  imasring  13993  qusring2  13995  opprrngbg  14007  dvdsrvald  14022  dvdsrd  14023  dvdsrex  14027  dvdsrtr  14030  unitgrp  14045  unitpropdg  14077  rhmopp  14105  isnzr2  14113  issubrng2  14139  subrngintm  14141  subrgintm  14172  rhmpropd  14183  aprap  14215  lmodprop2d  14277  rmodislmodlem  14279  lssvacl  14294  lssvsubcl  14295  lssvscl  14304  islss3  14308  lsspropdg  14360  rnglidlmcl  14409  2idlcpblrng  14452  crngridl  14459  expghmap  14536  mulgghm2  14537  mulgrhm  14538  znf1o  14580  znleval  14582  znidom  14586  psrval  14595  mplsubgfilemcl  14628  epttop  14729  topssnei  14801  restbasg  14807  restopnb  14820  cnfval  14833  cnpfval  14834  iscnp4  14857  cnpnei  14858  cnptopco  14861  cncnp  14869  cnrest2  14875  cnptoprest  14878  cnptoprest2  14879  lmss  14885  lmtopcnp  14889  neitx  14907  txcnp  14910  txrest  14915  txdis  14916  txlm  14918  cnmpt21  14930  imasnopn  14938  xmetres2  15018  blvalps  15027  blval  15028  bl2in  15042  blhalf  15047  blssps  15066  blss  15067  blssexps  15068  blssex  15069  ssblex  15070  blin2  15071  metss2lem  15136  bdmetval  15139  bdmopn  15143  metrest  15145  xmetxp  15146  xmetxpbl  15147  xmettx  15149  metcnp3  15150  txmetcnp  15157  addcncntoplem  15200  elcncf2  15213  mulc1cncf  15228  cncfco  15230  cncfmet  15231  mulcncf  15247  dedekindeulemub  15257  dedekindeulemloc  15258  dedekindeulemlu  15260  dedekindeu  15262  suplociccex  15264  dedekindicclemub  15266  dedekindicclemloc  15267  dedekindicclemlu  15269  dedekindicc  15272  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthdec  15283  ivthreinc  15284  dich0  15291  limcimolemlt  15303  limcimo  15304  cnplimccntop  15309  limccnp2lem  15315  limccnp2cntop  15316  dvfvalap  15320  dvmptfsum  15364  dveflem  15365  plyco  15398  plycn  15401  plyrecj  15402  reeff1olem  15410  reeff1oleme  15411  eflt  15414  sin0pilem2  15421  pilem3  15422  ptolemy  15463  ioocosf1o  15493  cxplt  15555  cxple  15556  cxplt3  15559  apcxp2  15578  rprelogbmul  15594  rprelogbdiv  15596  logbgt0b  15605  logbgcd1irrap  15609  fsumdvdsmul  15630  perfectlem2  15639  lgsdir2lem5  15676  lgsdir  15679  lgsdi  15681  lgsne0  15682  gausslemma2dlem1f1o  15704  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  lgsquad2lem2  15726  lgsquad2  15727  2sqlem6  15764  2sqlem10  15769  upgredg  15907  nnti  16267  pwtrufal  16274  pwf1oexmid  16276  sssneq  16279  qdencn  16306  cvgcmp2n  16312  trilpolemlt1  16320  trirec0  16323  trirec0xor  16324  redc0  16336  reap0  16337  cndcap  16338  nconstwlpolemgt0  16343  neap0mkv  16348  supfz  16350  inffz  16351