Theorem simprl 531

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  990  simp1rl  1089  simp2rl  1093  simp3rl  1097  rmob  3138  elpr2elpr  3882  disjiun  4106  reg3exmidlemwe  4703  opabssxpd  4788  0xp  4832  imainss  5180  iotam  5346  fvmptt  5771  fcof1o  5964  isotr  5991  riota5f  6032  ovmpodf  6187  unielxp  6370  fnmpoovd  6413  1stconst  6419  2ndconst  6420  cnvf1olem  6422  fvn0elsupp  6453  suppcofn  6468  tfrlemi14d  6566  tfrexlem  6567  tfr1onlemres  6582  tfrcllemres  6595  tfrcldm  6596  frecabcl  6632  nnaordi  6743  swoer  6797  qliftfun  6853  ecopovsymg  6870  th3qlem1  6873  pw2f1odclem  7089  mapen  7101  mapxpen  7103  fidifsnen  7127  fisbth  7142  findcard2d  7150  findcard2sd  7151  diffisn  7152  diffifi  7153  ac6sfi  7157  fidcen  7158  fimax2gtri  7161  fientri3  7177  nnwetri  7178  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  fisseneq  7197  exmidssfi  7201  fidcenumlemrk  7226  fidcenumlemr  7227  isbth  7239  ordiso2  7328  difinfsnlem  7392  difinfinf  7394  ctmlemr  7401  ctssdccl  7404  fodjum  7439  fodju0  7440  omniwomnimkv  7460  exmidfodomrlemrALT  7508  netap  7573  exmidmotap  7580  cc1  7584  cc2lem  7585  cc3  7587  cc4f  7588  cc4n  7590  dfplpq2  7674  dfmpq2  7675  mulpipqqs  7693  distrnqg  7707  ltexnqq  7728  subhalfnqq  7734  distrnq0  7779  prarloclemup  7815  prarloclem3  7817  prarloc  7823  genplt2i  7830  nqprl  7871  nqpru  7872  prmuloc  7886  mullocpr  7891  distrlem4prl  7904  distrlem4pru  7905  ltaddpr  7917  ltexprlemopl  7921  ltexprlemlol  7922  ltexprlemopu  7923  ltexprlemupu  7924  ltexprlemrl  7930  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  ltaprlem  7938  ltaprg  7939  prplnqu  7940  addextpr  7941  recexprlemdisj  7950  recexprlemloc  7951  recexprlem1ssl  7953  aptiprleml  7959  aptiprlemu  7960  ltmprr  7962  archpr  7963  cauappcvgprlemopl  7966  cauappcvgprlemopu  7968  cauappcvgprlemdisj  7971  cauappcvgprlemloc  7972  cauappcvgprlem1  7979  cauappcvgprlem2  7980  cauappcvgprlemlim  7981  caucvgprlemnkj  7986  caucvgprlemopl  7989  caucvgprlemopu  7991  caucvgprlemdisj  7994  caucvgprlemloc  7995  caucvgprlem2  8000  caucvgprprlemnkltj  8009  caucvgprprlemnkeqj  8010  caucvgprprlemnjltk  8011  caucvgprprlemmu  8015  caucvgprprlemopl  8017  caucvgprprlemopu  8019  caucvgprprlemdisj  8022  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  caucvgprprlemaddq  8028  caucvgprprlem2  8030  suplocexprlemrl  8037  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemex  8042  suplocexprlemub  8043  suplocexprlemlub  8044  recexgt0sr  8093  mulgt0sr  8098  prsrriota  8108  caucvgsrlemoffres  8120  suplocsrlem  8128  cnm  8152  addcnsr  8154  mulcnsr  8155  mulcnsrec  8163  axaddcl  8184  axmulcl  8186  axmulcom  8191  rereceu  8209  recriota  8210  axcaucvglemres  8219  axpre-suploclemres  8221  lelttr  8367  ltletr  8368  readdcan  8418  addcan  8458  addcan2  8459  addsub4  8521  ltadd2  8698  le2add  8723  lt2add  8724  lt2sub  8739  le2sub  8740  eqord1  8762  rimul  8864  rereim  8865  ltmul1  8871  apreim  8882  mulreim  8883  apcotr  8886  apadd1  8887  addext  8889  apneg  8890  mulext1  8891  mulext  8893  ltleap  8911  aprcl  8925  mulap0  8933  mulcanapd  8940  receuap  8948  recapb  8950  rec11ap  8989  rec11rap  8990  divdivdivap  8992  ddcanap  9005  divadddivap  9006  conjmulap  9008  subrecap  9118  prodgt0gt0  9130  prodge0  9133  ltmul12a  9139  lemulge11  9145  lt2mul2div  9158  ltrec  9162  lerec  9163  lt2msq  9165  lerec2  9168  le2msq  9180  msq11  9181  ledivp1  9182  mulle0r  9223  suprzclex  9682  peano5uzti  9692  supinfneg  9933  infsupneg  9934  qapne  9977  xrlelttr  10145  xrltletr  10146  xrre  10159  xaddge0  10217  xle2add  10218  xlt2add  10219  divelunit  10341  fzass4  10402  fzocatel  10551  zsupcllemstep  10596  zssinfcl  10599  suprzubdc  10603  zsupssdc  10605  suprzcl2dc  10606  exbtwnzlemex  10616  rebtwn2z  10621  qbtwnre  10623  modqid  10718  modqcyc  10728  modqaddabs  10731  modqaddmod  10732  mulqaddmodid  10733  modqadd2mod  10743  modqltm1p1mod  10745  modqsubmod  10751  modqsubmodmod  10752  modqmulmod  10758  modqmulmodr  10759  modqaddmulmod  10760  modqsubdir  10762  frec2uzisod  10776  iseqovex  10827  seqvalcd  10830  seq1g  10832  seqf  10833  seqovcd  10836  seqm1g  10843  seq3fveq2  10844  seq3shft2  10850  seqshft2g  10851  monoord  10854  seq3split  10857  seqsplitg  10858  iseqf1olemnab  10870  seqf1oglem1  10888  seqf1og  10890  seq3id2  10895  seqhomog  10899  seq3distr  10901  expcl2lemap  10920  expnegzap  10942  ltexp2a  10960  le2sq2  10984  nn0ltexp2  11079  nn0opth2  11094  bcval5  11133  hashcl  11152  hashen  11155  fihashdom  11175  hashunlem  11176  hashun  11177  hashmap  11200  fimaxq  11202  hashfibclem  11214  hashfibc  11215  zfz1isolem1  11220  zfz1iso  11221  lencl  11236  sswrd  11241  fstwrdne0  11272  lswlgt0cl  11285  ccatw2s1p1g  11341  ccat2s1fstg  11344  swrdval  11348  wrdind  11422  wrd2ind  11423  swrdccatfn  11424  swrdccatin1  11425  swrdccatin2  11429  pfxccatin12lem2  11431  pfxccatin12  11433  pfxccat3a  11438  reuccatpfxs1  11447  cvg1nlemres  11678  cvg1n  11679  recvguniq  11688  resqrexlemp1rp  11699  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemex  11718  sqrtmul  11728  sqrtsq  11737  absexpzap  11773  absle  11782  abs3lem  11804  amgm2  11811  maxleastlt  11908  maxltsup  11911  fimaxre2  11920  xrmaxleastlt  11949  xrmaxltsup  11951  xrmaxaddlem  11953  climcn2  12002  addcn2  12003  mulcn2  12005  reccn2ap  12006  climcau  12040  summodclem2  12076  summodc  12077  fsumf1o  12084  fisumss  12086  fsum3cvg3  12090  fsumcl2lem  12092  fsumadd  12100  fsum2dlemstep  12128  mptfzshft  12136  fsumrev  12137  fsummulc2  12142  modfsummod  12152  fsumrelem  12165  binom  12178  cvgratnn  12225  mertenslemub  12228  prodmodc  12272  zproddc  12273  fprodf1o  12282  fprodssdc  12284  fprodmul  12285  fprodrev  12313  fprod2dlemstep  12316  efcllem  12353  tanaddaplem  12432  dvdsval2  12484  moddvds  12493  dvdsabseq  12541  dvdsflip  12545  oexpneg  12571  fldivndvdslt  12631  bitsfi  12651  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemeu  12711  dfgcd3  12714  bezout  12715  dvdsmulgcd  12729  bezoutr  12736  nninfctlemfo  12744  ialgrlem1st  12747  lcmgcdlem  12782  coprmdvds2  12798  qredeu  12802  rpdvds  12804  isprm5lem  12846  isprm6  12852  pw2dvdslemn  12870  nonsq  12912  crth  12929  eulerthlemh  12936  pclemdc  12994  pcprendvds2  12997  pceu  13001  pcval  13002  pczpre  13003  pcmul  13007  pcqmul  13009  pcqcl  13012  pcid  13030  pcneg  13031  pcgcd1  13034  pc2dvds  13036  pcprmpw2  13039  difsqpwdvds  13044  pcmpt  13049  pockthg  13063  1arith  13073  mul4sq  13100  4sqexercise2  13105  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemg  13175  ennnfonelemex  13186  ennnfonelemrnh  13188  ennnfonelemrn  13191  ennnfonelemdm  13192  ennnfonelemnn0  13194  ennnfonelemim  13196  ennnfone  13197  ctinfomlemom  13199  ctinf  13202  ctiunctlemfo  13211  nninfdclemcl  13220  nninfdclemf  13221  nninfdclemp1  13222  unbendc  13226  isstruct2r  13244  setscom  13273  qusval  13557  ercpbl  13565  opifismgmdc  13605  grpinvalem  13619  grprida  13621  igsumvalx  13623  gsumfzval  13625  gsumpropd2  13627  gsumval2  13631  sgrppropd  13647  prdssgrpd  13649  mndpropd  13674  issubmnd  13676  submnd0  13678  prdsmndd  13682  mhmf1o  13704  0mhm  13720  resmhm  13721  mhmco  13724  mhmima  13725  mhmeql  13726  gsumwsubmcl  13730  gsumfzcl  13733  grppropd  13751  grpinvid1  13786  grpinvid2  13787  grplcan  13796  grplmulf1o  13808  grpnpncan0  13830  dfgrp3mlem  13832  grplactcnv  13836  pwssub  13847  mulgval  13860  mulgfng  13862  mulg1  13867  mulgnnp1  13868  mulgneg  13878  mulgnndir  13889  mulgdirlem  13891  mulgnn0ass  13896  mulgass  13897  subgmulg  13926  issubg4m  13931  subgintm  13936  0nsg  13952  eqgcpbl  13966  ghmmulg  13994  ghmpreima  14004  ghmeql  14005  ghmnsgima  14006  ghmnsgpreima  14007  ghmf1  14011  ghmf1o  14013  conjghm  14014  conjnmzb  14018  qusghm  14020  ablpncan3  14055  invghm  14067  eqgabl  14068  qusecsub  14069  gsumfzreidx  14075  gsumfzsubmcl  14076  gsumfzmptfidmadd  14077  gsumfzmhm  14081  imasrng  14121  qusrng  14123  srglmhm  14158  srgrmhm  14159  ringpropd  14203  ringlghm  14226  ringrghm  14227  imasring  14229  qusring2  14231  opprrngbg  14243  dvdsrvald  14260  dvdsrd  14261  dvdsrex  14265  dvdsrtr  14268  unitgrp  14283  unitpropdg  14315  rhmopp  14343  isnzr2  14351  issubrng2  14378  subrngintm  14380  subrgintm  14411  rhmpropd  14422  ringunitap  14453  aprap  14458  drngunitap  14468  lmodprop2d  14545  rmodislmodlem  14547  lssvacl  14562  lssvsubcl  14563  lssvscl  14572  islss3  14576  lsspropdg  14628  rnglidlmcl  14677  2idlcpblrng  14720  crngridl  14727  expghmap  14804  mulgghm2  14805  mulgrhm  14806  znf1o  14848  znleval  14850  znidom  14854  psrval  14863  psrbagcon  14875  psrbagconf1o  14877  mplsubgfilemcl  14903  epttop  15004  topssnei  15076  restbasg  15082  restopnb  15095  cnfval  15108  cnpfval  15109  iscnp4  15132  cnpnei  15133  cnptopco  15136  cncnp  15144  cnrest2  15150  cnptoprest  15153  cnptoprest2  15154  lmss  15160  lmtopcnp  15164  neitx  15182  txcnp  15185  txrest  15190  txdis  15191  txlm  15193  cnmpt21  15205  imasnopn  15213  xmetres2  15293  blvalps  15302  blval  15303  bl2in  15317  blhalf  15322  blssps  15341  blss  15342  blssexps  15343  blssex  15344  ssblex  15345  blin2  15346  metss2lem  15411  bdmetval  15414  bdmopn  15418  metrest  15420  xmetxp  15421  xmetxpbl  15422  xmettx  15424  metcnp3  15425  txmetcnp  15432  addcncntoplem  15475  elcncf2  15488  mulc1cncf  15503  cncfco  15505  cncfmet  15506  mulcncf  15522  dedekindeulemub  15532  dedekindeulemloc  15533  dedekindeulemlu  15535  dedekindeu  15537  suplociccex  15539  dedekindicclemub  15541  dedekindicclemloc  15542  dedekindicclemlu  15544  dedekindicc  15547  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthdec  15558  ivthreinc  15559  dich0  15566  limcimolemlt  15578  limcimo  15579  cnplimccntop  15584  limccnp2lem  15590  limccnp2cntop  15591  dvfvalap  15595  dvmptfsum  15639  dveflem  15640  plyco  15673  plycn  15676  plyrecj  15677  reeff1olem  15685  reeff1oleme  15686  eflt  15689  sin0pilem2  15696  pilem3  15697  ptolemy  15738  ioocosf1o  15768  cxplt  15830  cxple  15831  cxplt3  15834  apcxp2  15853  rprelogbmul  15869  rprelogbdiv  15871  logbgt0b  15880  logbgcd1irrap  15884  pellexlem3  15896  fsumdvdsmul  15908  perfectlem2  15917  lgsdir2lem5  15954  lgsdir  15957  lgsdi  15959  lgsne0  15960  gausslemma2dlem1f1o  15982  lgseisenlem2  15993  lgsquadlem1  15999  lgsquadlem2  16000  lgsquad2lem2  16004  lgsquad2  16005  2sqlem6  16042  2sqlem10  16047  upgredg  16188  uhgrissubgr  16305  subgrprop3  16306  upgrspanop  16327  umgrspanop  16328  usgrspanop  16329  vtxedgfi  16333  vtxlpfi  16334  upgr2wlkdc  16421  clwwlkccatlem  16444  eupth2lemsfi  16522  depindlem3  16552  nnti  16815  pwtrufal  16820  pwf1oexmid  16822  sssneq  16825  qdencn  16856  cvgcmp2n  16866  trilpolemlt1  16874  trirec0  16877  trirec0xor  16878  qdiff  16882  redc0  16891  reap0  16892  cndcap  16893  trimul0or  16894  nconstwlpolemgt0  16899  neap0mkv  16904  supfz  16906  inffz  16907  gfsumval  16911  gfsumcl  16919