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:  dfifp2dc  987  simp1rl  1086  simp2rl  1090  simp3rl  1094  rmob  3122  elpr2elpr  3854  disjiun  4078  reg3exmidlemwe  4671  0xp  4799  imainss  5144  iotam  5310  fvmptt  5728  fcof1o  5919  isotr  5946  riota5f  5987  ovmpodf  6142  unielxp  6326  fnmpoovd  6367  1stconst  6373  2ndconst  6374  cnvf1olem  6376  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemres  6501  tfrcllemres  6514  tfrcldm  6515  frecabcl  6551  nnaordi  6662  swoer  6716  qliftfun  6772  ecopovsymg  6789  th3qlem1  6792  pw2f1odclem  7003  mapen  7015  mapxpen  7017  fidifsnen  7040  fisbth  7053  findcard2d  7061  findcard2sd  7062  diffisn  7063  diffifi  7064  ac6sfi  7068  fimax2gtri  7071  fientri3  7085  nnwetri  7086  unsnfi  7089  unsnfidcex  7090  unsnfidcel  7091  fisseneq  7104  fidcenumlemrk  7129  fidcenumlemr  7130  isbth  7142  ordiso2  7210  difinfsnlem  7274  difinfinf  7276  ctmlemr  7283  ctssdccl  7286  fodjum  7321  fodju0  7322  omniwomnimkv  7342  exmidfodomrlemrALT  7389  netap  7448  exmidmotap  7455  cc1  7459  cc2lem  7460  cc3  7462  cc4f  7463  cc4n  7465  dfplpq2  7549  dfmpq2  7550  mulpipqqs  7568  distrnqg  7582  ltexnqq  7603  subhalfnqq  7609  distrnq0  7654  prarloclemup  7690  prarloclem3  7692  prarloc  7698  genplt2i  7705  nqprl  7746  nqpru  7747  prmuloc  7761  mullocpr  7766  distrlem4prl  7779  distrlem4pru  7780  ltaddpr  7792  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  ltaprlem  7813  ltaprg  7814  prplnqu  7815  addextpr  7816  recexprlemdisj  7825  recexprlemloc  7826  recexprlem1ssl  7828  aptiprleml  7834  aptiprlemu  7835  ltmprr  7837  archpr  7838  cauappcvgprlemopl  7841  cauappcvgprlemopu  7843  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlem1  7854  cauappcvgprlem2  7855  cauappcvgprlemlim  7856  caucvgprlemnkj  7861  caucvgprlemopl  7864  caucvgprlemopu  7866  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprlem2  7875  caucvgprprlemnkltj  7884  caucvgprprlemnkeqj  7885  caucvgprprlemnjltk  7886  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemopu  7894  caucvgprprlemdisj  7897  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  caucvgprprlemaddq  7903  caucvgprprlem2  7905  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemex  7917  suplocexprlemub  7918  suplocexprlemlub  7919  recexgt0sr  7968  mulgt0sr  7973  prsrriota  7983  caucvgsrlemoffres  7995  suplocsrlem  8003  cnm  8027  addcnsr  8029  mulcnsr  8030  mulcnsrec  8038  axaddcl  8059  axmulcl  8061  axmulcom  8066  rereceu  8084  recriota  8085  axcaucvglemres  8094  axpre-suploclemres  8096  lelttr  8243  ltletr  8244  readdcan  8294  addcan  8334  addcan2  8335  addsub4  8397  ltadd2  8574  le2add  8599  lt2add  8600  lt2sub  8615  le2sub  8616  eqord1  8638  rimul  8740  rereim  8741  ltmul1  8747  apreim  8758  mulreim  8759  apcotr  8762  apadd1  8763  addext  8765  apneg  8766  mulext1  8767  mulext  8769  ltleap  8787  aprcl  8801  mulap0  8809  mulcanapd  8816  receuap  8824  recapb  8826  rec11ap  8865  rec11rap  8866  divdivdivap  8868  ddcanap  8881  divadddivap  8882  conjmulap  8884  subrecap  8994  prodgt0gt0  9006  prodge0  9009  ltmul12a  9015  lemulge11  9021  lt2mul2div  9034  ltrec  9038  lerec  9039  lt2msq  9041  lerec2  9044  le2msq  9056  msq11  9057  ledivp1  9058  mulle0r  9099  suprzclex  9553  peano5uzti  9563  supinfneg  9798  infsupneg  9799  qapne  9842  xrlelttr  10010  xrltletr  10011  xrre  10024  xaddge0  10082  xle2add  10083  xlt2add  10084  divelunit  10206  fzass4  10266  fzocatel  10413  zsupcllemstep  10457  zssinfcl  10460  suprzubdc  10464  zsupssdc  10466  suprzcl2dc  10467  exbtwnzlemex  10477  rebtwn2z  10482  qbtwnre  10484  modqid  10579  modqcyc  10589  modqaddabs  10592  modqaddmod  10593  mulqaddmodid  10594  modqadd2mod  10604  modqltm1p1mod  10606  modqsubmod  10612  modqsubmodmod  10613  modqmulmod  10619  modqmulmodr  10620  modqaddmulmod  10621  modqsubdir  10623  frec2uzisod  10637  iseqovex  10688  seqvalcd  10691  seq1g  10693  seqf  10694  seqovcd  10697  seqm1g  10704  seq3fveq2  10705  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  iseqf1olemnab  10731  seqf1oglem1  10749  seqf1og  10751  seq3id2  10756  seqhomog  10760  seq3distr  10762  expcl2lemap  10781  expnegzap  10803  ltexp2a  10821  le2sq2  10845  nn0ltexp2  10939  nn0opth2  10954  bcval5  10993  hashcl  11011  hashen  11014  fihashdom  11033  hashunlem  11034  hashun  11035  fimaxq  11057  zfz1isolem1  11070  zfz1iso  11071  lencl  11083  sswrd  11088  fstwrdne0  11119  lswlgt0cl  11132  swrdval  11188  wrdind  11262  wrd2ind  11263  swrdccatfn  11264  swrdccatin1  11265  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12  11273  pfxccat3a  11278  reuccatpfxs1  11287  cvg1nlemres  11504  cvg1n  11505  recvguniq  11514  resqrexlemp1rp  11525  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemex  11544  sqrtmul  11554  sqrtsq  11563  absexpzap  11599  absle  11608  abs3lem  11630  amgm2  11637  maxleastlt  11734  maxltsup  11737  fimaxre2  11746  xrmaxleastlt  11775  xrmaxltsup  11777  xrmaxaddlem  11779  climcn2  11828  addcn2  11829  mulcn2  11831  reccn2ap  11832  climcau  11866  summodclem2  11901  summodc  11902  fsumf1o  11909  fisumss  11911  fsum3cvg3  11915  fsumcl2lem  11917  fsumadd  11925  fsum2dlemstep  11953  mptfzshft  11961  fsumrev  11962  fsummulc2  11967  modfsummod  11977  fsumrelem  11990  binom  12003  cvgratnn  12050  mertenslemub  12053  prodmodc  12097  zproddc  12098  fprodf1o  12107  fprodssdc  12109  fprodmul  12110  fprodrev  12138  fprod2dlemstep  12141  efcllem  12178  tanaddaplem  12257  dvdsval2  12309  moddvds  12318  dvdsabseq  12366  dvdsflip  12370  oexpneg  12396  fldivndvdslt  12456  bitsfi  12476  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemeu  12536  dfgcd3  12539  bezout  12540  dvdsmulgcd  12554  bezoutr  12561  nninfctlemfo  12569  ialgrlem1st  12572  lcmgcdlem  12607  coprmdvds2  12623  qredeu  12627  rpdvds  12629  isprm5lem  12671  isprm6  12677  pw2dvdslemn  12695  nonsq  12737  crth  12754  eulerthlemh  12761  pclemdc  12819  pcprendvds2  12822  pceu  12826  pcval  12827  pczpre  12828  pcmul  12832  pcqmul  12834  pcqcl  12837  pcid  12855  pcneg  12856  pcgcd1  12859  pc2dvds  12861  pcprmpw2  12864  difsqpwdvds  12869  pcmpt  12874  pockthg  12888  1arith  12898  mul4sq  12925  4sqexercise2  12930  ennnfonelemg  12982  ennnfonelemex  12993  ennnfonelemrnh  12995  ennnfonelemrn  12998  ennnfonelemdm  12999  ennnfonelemnn0  13001  ennnfonelemim  13003  ennnfone  13004  ctinfomlemom  13006  ctinf  13009  ctiunctlemfo  13018  nninfdclemcl  13027  nninfdclemf  13028  nninfdclemp1  13029  unbendc  13033  isstruct2r  13051  setscom  13080  qusval  13364  ercpbl  13372  opifismgmdc  13412  grpinvalem  13426  grprida  13428  igsumvalx  13430  gsumfzval  13432  gsumpropd2  13434  gsumval2  13438  sgrppropd  13454  prdssgrpd  13456  mndpropd  13481  issubmnd  13483  submnd0  13485  prdsmndd  13489  mhmf1o  13511  0mhm  13527  resmhm  13528  mhmco  13531  mhmima  13532  mhmeql  13533  gsumwsubmcl  13537  gsumfzcl  13540  grppropd  13558  grpinvid1  13593  grpinvid2  13594  grplcan  13603  grplmulf1o  13615  grpnpncan0  13637  dfgrp3mlem  13639  grplactcnv  13643  pwssub  13654  mulgval  13667  mulgfng  13669  mulg1  13674  mulgnnp1  13675  mulgneg  13685  mulgnndir  13696  mulgdirlem  13698  mulgnn0ass  13703  mulgass  13704  subgmulg  13733  issubg4m  13738  subgintm  13743  0nsg  13759  eqgcpbl  13773  ghmmulg  13801  ghmpreima  13811  ghmeql  13812  ghmnsgima  13813  ghmnsgpreima  13814  ghmf1  13818  ghmf1o  13820  conjghm  13821  conjnmzb  13825  qusghm  13827  ablpncan3  13862  invghm  13874  eqgabl  13875  qusecsub  13876  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  imasrng  13927  qusrng  13929  srglmhm  13964  srgrmhm  13965  ringpropd  14009  ringlghm  14032  ringrghm  14033  imasring  14035  qusring2  14037  opprrngbg  14049  dvdsrvald  14065  dvdsrd  14066  dvdsrex  14070  dvdsrtr  14073  unitgrp  14088  unitpropdg  14120  rhmopp  14148  isnzr2  14156  issubrng2  14182  subrngintm  14184  subrgintm  14215  rhmpropd  14226  aprap  14258  lmodprop2d  14320  rmodislmodlem  14322  lssvacl  14337  lssvsubcl  14338  lssvscl  14347  islss3  14351  lsspropdg  14403  rnglidlmcl  14452  2idlcpblrng  14495  crngridl  14502  expghmap  14579  mulgghm2  14580  mulgrhm  14581  znf1o  14623  znleval  14625  znidom  14629  psrval  14638  mplsubgfilemcl  14671  epttop  14772  topssnei  14844  restbasg  14850  restopnb  14863  cnfval  14876  cnpfval  14877  iscnp4  14900  cnpnei  14901  cnptopco  14904  cncnp  14912  cnrest2  14918  cnptoprest  14921  cnptoprest2  14922  lmss  14928  lmtopcnp  14932  neitx  14950  txcnp  14953  txrest  14958  txdis  14959  txlm  14961  cnmpt21  14973  imasnopn  14981  xmetres2  15061  blvalps  15070  blval  15071  bl2in  15085  blhalf  15090  blssps  15109  blss  15110  blssexps  15111  blssex  15112  ssblex  15113  blin2  15114  metss2lem  15179  bdmetval  15182  bdmopn  15186  metrest  15188  xmetxp  15189  xmetxpbl  15190  xmettx  15192  metcnp3  15193  txmetcnp  15200  addcncntoplem  15243  elcncf2  15256  mulc1cncf  15271  cncfco  15273  cncfmet  15274  mulcncf  15290  dedekindeulemub  15300  dedekindeulemloc  15301  dedekindeulemlu  15303  dedekindeu  15305  suplociccex  15307  dedekindicclemub  15309  dedekindicclemloc  15310  dedekindicclemlu  15312  dedekindicc  15315  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthdec  15326  ivthreinc  15327  dich0  15334  limcimolemlt  15346  limcimo  15347  cnplimccntop  15352  limccnp2lem  15358  limccnp2cntop  15359  dvfvalap  15363  dvmptfsum  15407  dveflem  15408  plyco  15441  plycn  15444  plyrecj  15445  reeff1olem  15453  reeff1oleme  15454  eflt  15457  sin0pilem2  15464  pilem3  15465  ptolemy  15506  ioocosf1o  15536  cxplt  15598  cxple  15599  cxplt3  15602  apcxp2  15621  rprelogbmul  15637  rprelogbdiv  15639  logbgt0b  15648  logbgcd1irrap  15652  fsumdvdsmul  15673  perfectlem2  15682  lgsdir2lem5  15719  lgsdir  15722  lgsdi  15724  lgsne0  15725  gausslemma2dlem1f1o  15747  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem2  15769  lgsquad2  15770  2sqlem6  15807  2sqlem10  15812  upgredg  15950  upgr2wlkdc  16096  fidcen  16379  nnti  16385  pwtrufal  16392  pwf1oexmid  16394  sssneq  16397  qdencn  16425  cvgcmp2n  16431  trilpolemlt1  16439  trirec0  16442  trirec0xor  16443  redc0  16455  reap0  16456  cndcap  16457  nconstwlpolemgt0  16462  neap0mkv  16467  supfz  16469  inffz  16470