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  3123  elpr2elpr  3857  disjiun  4081  reg3exmidlemwe  4675  opabssxpd  4760  0xp  4804  imainss  5150  iotam  5316  fvmptt  5734  fcof1o  5925  isotr  5952  riota5f  5993  ovmpodf  6148  unielxp  6332  fnmpoovd  6375  1stconst  6381  2ndconst  6382  cnvf1olem  6384  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemres  6510  tfrcllemres  6523  tfrcldm  6524  frecabcl  6560  nnaordi  6671  swoer  6725  qliftfun  6781  ecopovsymg  6798  th3qlem1  6801  pw2f1odclem  7015  mapen  7027  mapxpen  7029  fidifsnen  7052  fisbth  7067  findcard2d  7075  findcard2sd  7076  diffisn  7077  diffifi  7078  ac6sfi  7082  fidcen  7083  fimax2gtri  7086  fientri3  7102  nnwetri  7103  unsnfi  7106  unsnfidcex  7107  unsnfidcel  7108  fisseneq  7121  exmidssfi  7125  fidcenumlemrk  7147  fidcenumlemr  7148  isbth  7160  ordiso2  7228  difinfsnlem  7292  difinfinf  7294  ctmlemr  7301  ctssdccl  7304  fodjum  7339  fodju0  7340  omniwomnimkv  7360  exmidfodomrlemrALT  7407  netap  7466  exmidmotap  7473  cc1  7477  cc2lem  7478  cc3  7480  cc4f  7481  cc4n  7483  dfplpq2  7567  dfmpq2  7568  mulpipqqs  7586  distrnqg  7600  ltexnqq  7621  subhalfnqq  7627  distrnq0  7672  prarloclemup  7708  prarloclem3  7710  prarloc  7716  genplt2i  7723  nqprl  7764  nqpru  7765  prmuloc  7779  mullocpr  7784  distrlem4prl  7797  distrlem4pru  7798  ltaddpr  7810  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  ltaprlem  7831  ltaprg  7832  prplnqu  7833  addextpr  7834  recexprlemdisj  7843  recexprlemloc  7844  recexprlem1ssl  7846  aptiprleml  7852  aptiprlemu  7853  ltmprr  7855  archpr  7856  cauappcvgprlemopl  7859  cauappcvgprlemopu  7861  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlem1  7872  cauappcvgprlem2  7873  cauappcvgprlemlim  7874  caucvgprlemnkj  7879  caucvgprlemopl  7882  caucvgprlemopu  7884  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprlem2  7893  caucvgprprlemnkltj  7902  caucvgprprlemnkeqj  7903  caucvgprprlemnjltk  7904  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemopu  7912  caucvgprprlemdisj  7915  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  caucvgprprlemaddq  7921  caucvgprprlem2  7923  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemex  7935  suplocexprlemub  7936  suplocexprlemlub  7937  recexgt0sr  7986  mulgt0sr  7991  prsrriota  8001  caucvgsrlemoffres  8013  suplocsrlem  8021  cnm  8045  addcnsr  8047  mulcnsr  8048  mulcnsrec  8056  axaddcl  8077  axmulcl  8079  axmulcom  8084  rereceu  8102  recriota  8103  axcaucvglemres  8112  axpre-suploclemres  8114  lelttr  8261  ltletr  8262  readdcan  8312  addcan  8352  addcan2  8353  addsub4  8415  ltadd2  8592  le2add  8617  lt2add  8618  lt2sub  8633  le2sub  8634  eqord1  8656  rimul  8758  rereim  8759  ltmul1  8765  apreim  8776  mulreim  8777  apcotr  8780  apadd1  8781  addext  8783  apneg  8784  mulext1  8785  mulext  8787  ltleap  8805  aprcl  8819  mulap0  8827  mulcanapd  8834  receuap  8842  recapb  8844  rec11ap  8883  rec11rap  8884  divdivdivap  8886  ddcanap  8899  divadddivap  8900  conjmulap  8902  subrecap  9012  prodgt0gt0  9024  prodge0  9027  ltmul12a  9033  lemulge11  9039  lt2mul2div  9052  ltrec  9056  lerec  9057  lt2msq  9059  lerec2  9062  le2msq  9074  msq11  9075  ledivp1  9076  mulle0r  9117  suprzclex  9571  peano5uzti  9581  supinfneg  9822  infsupneg  9823  qapne  9866  xrlelttr  10034  xrltletr  10035  xrre  10048  xaddge0  10106  xle2add  10107  xlt2add  10108  divelunit  10230  fzass4  10290  fzocatel  10437  zsupcllemstep  10482  zssinfcl  10485  suprzubdc  10489  zsupssdc  10491  suprzcl2dc  10492  exbtwnzlemex  10502  rebtwn2z  10507  qbtwnre  10509  modqid  10604  modqcyc  10614  modqaddabs  10617  modqaddmod  10618  mulqaddmodid  10619  modqadd2mod  10629  modqltm1p1mod  10631  modqsubmod  10637  modqsubmodmod  10638  modqmulmod  10644  modqmulmodr  10645  modqaddmulmod  10646  modqsubdir  10648  frec2uzisod  10662  iseqovex  10713  seqvalcd  10716  seq1g  10718  seqf  10719  seqovcd  10722  seqm1g  10729  seq3fveq2  10730  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  iseqf1olemnab  10756  seqf1oglem1  10774  seqf1og  10776  seq3id2  10781  seqhomog  10785  seq3distr  10787  expcl2lemap  10806  expnegzap  10828  ltexp2a  10846  le2sq2  10870  nn0ltexp2  10964  nn0opth2  10979  bcval5  11018  hashcl  11036  hashen  11039  fihashdom  11059  hashunlem  11060  hashun  11061  fimaxq  11084  zfz1isolem1  11097  zfz1iso  11098  lencl  11110  sswrd  11115  fstwrdne0  11146  lswlgt0cl  11159  ccatw2s1p1g  11215  ccat2s1fstg  11218  swrdval  11222  wrdind  11296  wrd2ind  11297  swrdccatfn  11298  swrdccatin1  11299  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12  11307  pfxccat3a  11312  reuccatpfxs1  11321  cvg1nlemres  11539  cvg1n  11540  recvguniq  11549  resqrexlemp1rp  11560  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemex  11579  sqrtmul  11589  sqrtsq  11598  absexpzap  11634  absle  11643  abs3lem  11665  amgm2  11672  maxleastlt  11769  maxltsup  11772  fimaxre2  11781  xrmaxleastlt  11810  xrmaxltsup  11812  xrmaxaddlem  11814  climcn2  11863  addcn2  11864  mulcn2  11866  reccn2ap  11867  climcau  11901  summodclem2  11936  summodc  11937  fsumf1o  11944  fisumss  11946  fsum3cvg3  11950  fsumcl2lem  11952  fsumadd  11960  fsum2dlemstep  11988  mptfzshft  11996  fsumrev  11997  fsummulc2  12002  modfsummod  12012  fsumrelem  12025  binom  12038  cvgratnn  12085  mertenslemub  12088  prodmodc  12132  zproddc  12133  fprodf1o  12142  fprodssdc  12144  fprodmul  12145  fprodrev  12173  fprod2dlemstep  12176  efcllem  12213  tanaddaplem  12292  dvdsval2  12344  moddvds  12353  dvdsabseq  12401  dvdsflip  12405  oexpneg  12431  fldivndvdslt  12491  bitsfi  12511  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemeu  12571  dfgcd3  12574  bezout  12575  dvdsmulgcd  12589  bezoutr  12596  nninfctlemfo  12604  ialgrlem1st  12607  lcmgcdlem  12642  coprmdvds2  12658  qredeu  12662  rpdvds  12664  isprm5lem  12706  isprm6  12712  pw2dvdslemn  12730  nonsq  12772  crth  12789  eulerthlemh  12796  pclemdc  12854  pcprendvds2  12857  pceu  12861  pcval  12862  pczpre  12863  pcmul  12867  pcqmul  12869  pcqcl  12872  pcid  12890  pcneg  12891  pcgcd1  12894  pc2dvds  12896  pcprmpw2  12899  difsqpwdvds  12904  pcmpt  12909  pockthg  12923  1arith  12933  mul4sq  12960  4sqexercise2  12965  ennnfonelemg  13017  ennnfonelemex  13028  ennnfonelemrnh  13030  ennnfonelemrn  13033  ennnfonelemdm  13034  ennnfonelemnn0  13036  ennnfonelemim  13038  ennnfone  13039  ctinfomlemom  13041  ctinf  13044  ctiunctlemfo  13053  nninfdclemcl  13062  nninfdclemf  13063  nninfdclemp1  13064  unbendc  13068  isstruct2r  13086  setscom  13115  qusval  13399  ercpbl  13407  opifismgmdc  13447  grpinvalem  13461  grprida  13463  igsumvalx  13465  gsumfzval  13467  gsumpropd2  13469  gsumval2  13473  sgrppropd  13489  prdssgrpd  13491  mndpropd  13516  issubmnd  13518  submnd0  13520  prdsmndd  13524  mhmf1o  13546  0mhm  13562  resmhm  13563  mhmco  13566  mhmima  13567  mhmeql  13568  gsumwsubmcl  13572  gsumfzcl  13575  grppropd  13593  grpinvid1  13628  grpinvid2  13629  grplcan  13638  grplmulf1o  13650  grpnpncan0  13672  dfgrp3mlem  13674  grplactcnv  13678  pwssub  13689  mulgval  13702  mulgfng  13704  mulg1  13709  mulgnnp1  13710  mulgneg  13720  mulgnndir  13731  mulgdirlem  13733  mulgnn0ass  13738  mulgass  13739  subgmulg  13768  issubg4m  13773  subgintm  13778  0nsg  13794  eqgcpbl  13808  ghmmulg  13836  ghmpreima  13846  ghmeql  13847  ghmnsgima  13848  ghmnsgpreima  13849  ghmf1  13853  ghmf1o  13855  conjghm  13856  conjnmzb  13860  qusghm  13862  ablpncan3  13897  invghm  13909  eqgabl  13910  qusecsub  13911  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  imasrng  13962  qusrng  13964  srglmhm  13999  srgrmhm  14000  ringpropd  14044  ringlghm  14067  ringrghm  14068  imasring  14070  qusring2  14072  opprrngbg  14084  dvdsrvald  14100  dvdsrd  14101  dvdsrex  14105  dvdsrtr  14108  unitgrp  14123  unitpropdg  14155  rhmopp  14183  isnzr2  14191  issubrng2  14217  subrngintm  14219  subrgintm  14250  rhmpropd  14261  aprap  14293  lmodprop2d  14355  rmodislmodlem  14357  lssvacl  14372  lssvsubcl  14373  lssvscl  14382  islss3  14386  lsspropdg  14438  rnglidlmcl  14487  2idlcpblrng  14530  crngridl  14537  expghmap  14614  mulgghm2  14615  mulgrhm  14616  znf1o  14658  znleval  14660  znidom  14664  psrval  14673  mplsubgfilemcl  14706  epttop  14807  topssnei  14879  restbasg  14885  restopnb  14898  cnfval  14911  cnpfval  14912  iscnp4  14935  cnpnei  14936  cnptopco  14939  cncnp  14947  cnrest2  14953  cnptoprest  14956  cnptoprest2  14957  lmss  14963  lmtopcnp  14967  neitx  14985  txcnp  14988  txrest  14993  txdis  14994  txlm  14996  cnmpt21  15008  imasnopn  15016  xmetres2  15096  blvalps  15105  blval  15106  bl2in  15120  blhalf  15125  blssps  15144  blss  15145  blssexps  15146  blssex  15147  ssblex  15148  blin2  15149  metss2lem  15214  bdmetval  15217  bdmopn  15221  metrest  15223  xmetxp  15224  xmetxpbl  15225  xmettx  15227  metcnp3  15228  txmetcnp  15235  addcncntoplem  15278  elcncf2  15291  mulc1cncf  15306  cncfco  15308  cncfmet  15309  mulcncf  15325  dedekindeulemub  15335  dedekindeulemloc  15336  dedekindeulemlu  15338  dedekindeu  15340  suplociccex  15342  dedekindicclemub  15344  dedekindicclemloc  15345  dedekindicclemlu  15347  dedekindicc  15350  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthdec  15361  ivthreinc  15362  dich0  15369  limcimolemlt  15381  limcimo  15382  cnplimccntop  15387  limccnp2lem  15393  limccnp2cntop  15394  dvfvalap  15398  dvmptfsum  15442  dveflem  15443  plyco  15476  plycn  15479  plyrecj  15480  reeff1olem  15488  reeff1oleme  15489  eflt  15492  sin0pilem2  15499  pilem3  15500  ptolemy  15541  ioocosf1o  15571  cxplt  15633  cxple  15634  cxplt3  15637  apcxp2  15656  rprelogbmul  15672  rprelogbdiv  15674  logbgt0b  15683  logbgcd1irrap  15687  fsumdvdsmul  15708  perfectlem2  15717  lgsdir2lem5  15754  lgsdir  15757  lgsdi  15759  lgsne0  15760  gausslemma2dlem1f1o  15782  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem2  15804  lgsquad2  15805  2sqlem6  15842  2sqlem10  15847  upgredg  15988  vtxedgfi  16100  vtxlpfi  16101  upgr2wlkdc  16186  clwwlkccatlem  16209  nnti  16541  pwtrufal  16548  pwf1oexmid  16550  sssneq  16553  qdencn  16581  cvgcmp2n  16587  trilpolemlt1  16595  trirec0  16598  trirec0xor  16599  redc0  16611  reap0  16612  cndcap  16613  nconstwlpolemgt0  16618  neap0mkv  16623  supfz  16625  inffz  16626  gfsumval  16630