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  989  simp1rl  1088  simp2rl  1092  simp3rl  1096  rmob  3125  elpr2elpr  3859  disjiun  4083  reg3exmidlemwe  4677  opabssxpd  4762  0xp  4806  imainss  5152  iotam  5318  fvmptt  5738  fcof1o  5930  isotr  5957  riota5f  5998  ovmpodf  6153  unielxp  6337  fnmpoovd  6380  1stconst  6386  2ndconst  6387  cnvf1olem  6389  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemres  6515  tfrcllemres  6528  tfrcldm  6529  frecabcl  6565  nnaordi  6676  swoer  6730  qliftfun  6786  ecopovsymg  6803  th3qlem1  6806  pw2f1odclem  7020  mapen  7032  mapxpen  7034  fidifsnen  7057  fisbth  7072  findcard2d  7080  findcard2sd  7081  diffisn  7082  diffifi  7083  ac6sfi  7087  fidcen  7088  fimax2gtri  7091  fientri3  7107  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  exmidssfi  7131  fidcenumlemrk  7153  fidcenumlemr  7154  isbth  7166  ordiso2  7234  difinfsnlem  7298  difinfinf  7300  ctmlemr  7307  ctssdccl  7310  fodjum  7345  fodju0  7346  omniwomnimkv  7366  exmidfodomrlemrALT  7414  netap  7473  exmidmotap  7480  cc1  7484  cc2lem  7485  cc3  7487  cc4f  7488  cc4n  7490  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  ltexnqq  7628  subhalfnqq  7634  distrnq0  7679  prarloclemup  7715  prarloclem3  7717  prarloc  7723  genplt2i  7730  nqprl  7771  nqpru  7772  prmuloc  7786  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltaddpr  7817  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprlem  7838  ltaprg  7839  prplnqu  7840  addextpr  7841  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlem2  7900  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  recexgt0sr  7993  mulgt0sr  7998  prsrriota  8008  caucvgsrlemoffres  8020  suplocsrlem  8028  cnm  8052  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axaddcl  8084  axmulcl  8086  axmulcom  8091  rereceu  8109  recriota  8110  axcaucvglemres  8119  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  addsub4  8422  ltadd2  8599  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  eqord1  8663  rimul  8765  rereim  8766  ltmul1  8772  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  apneg  8791  mulext1  8792  mulext  8794  ltleap  8812  aprcl  8826  mulap0  8834  mulcanapd  8841  receuap  8849  recapb  8851  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  conjmulap  8909  subrecap  9019  prodgt0gt0  9031  prodge0  9034  ltmul12a  9040  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lt2msq  9066  lerec2  9069  le2msq  9081  msq11  9082  ledivp1  9083  mulle0r  9124  suprzclex  9578  peano5uzti  9588  supinfneg  9829  infsupneg  9830  qapne  9873  xrlelttr  10041  xrltletr  10042  xrre  10055  xaddge0  10113  xle2add  10114  xlt2add  10115  divelunit  10237  fzass4  10297  fzocatel  10445  zsupcllemstep  10490  zssinfcl  10493  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  exbtwnzlemex  10510  rebtwn2z  10515  qbtwnre  10517  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modqmulmod  10652  modqmulmodr  10653  modqaddmulmod  10654  modqsubdir  10656  frec2uzisod  10670  iseqovex  10721  seqvalcd  10724  seq1g  10726  seqf  10727  seqovcd  10730  seqm1g  10737  seq3fveq2  10738  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  iseqf1olemnab  10764  seqf1oglem1  10782  seqf1og  10784  seq3id2  10789  seqhomog  10793  seq3distr  10795  expcl2lemap  10814  expnegzap  10836  ltexp2a  10854  le2sq2  10878  nn0ltexp2  10972  nn0opth2  10987  bcval5  11026  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  fimaxq  11092  zfz1isolem1  11105  zfz1iso  11106  lencl  11118  sswrd  11123  fstwrdne0  11154  lswlgt0cl  11167  ccatw2s1p1g  11223  ccat2s1fstg  11226  swrdval  11230  wrdind  11304  wrd2ind  11305  swrdccatfn  11306  swrdccatin1  11307  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12  11315  pfxccat3a  11320  reuccatpfxs1  11329  cvg1nlemres  11547  cvg1n  11548  recvguniq  11557  resqrexlemp1rp  11568  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemex  11587  sqrtmul  11597  sqrtsq  11606  absexpzap  11642  absle  11651  abs3lem  11673  amgm2  11680  maxleastlt  11777  maxltsup  11780  fimaxre2  11789  xrmaxleastlt  11818  xrmaxltsup  11820  xrmaxaddlem  11822  climcn2  11871  addcn2  11872  mulcn2  11874  reccn2ap  11875  climcau  11909  summodclem2  11945  summodc  11946  fsumf1o  11953  fisumss  11955  fsum3cvg3  11959  fsumcl2lem  11961  fsumadd  11969  fsum2dlemstep  11997  mptfzshft  12005  fsumrev  12006  fsummulc2  12011  modfsummod  12021  fsumrelem  12034  binom  12047  cvgratnn  12094  mertenslemub  12097  prodmodc  12141  zproddc  12142  fprodf1o  12151  fprodssdc  12153  fprodmul  12154  fprodrev  12182  fprod2dlemstep  12185  efcllem  12222  tanaddaplem  12301  dvdsval2  12353  moddvds  12362  dvdsabseq  12410  dvdsflip  12414  oexpneg  12440  fldivndvdslt  12500  bitsfi  12520  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemeu  12580  dfgcd3  12583  bezout  12584  dvdsmulgcd  12598  bezoutr  12605  nninfctlemfo  12613  ialgrlem1st  12616  lcmgcdlem  12651  coprmdvds2  12667  qredeu  12671  rpdvds  12673  isprm5lem  12715  isprm6  12721  pw2dvdslemn  12739  nonsq  12781  crth  12798  eulerthlemh  12805  pclemdc  12863  pcprendvds2  12866  pceu  12870  pcval  12871  pczpre  12872  pcmul  12876  pcqmul  12878  pcqcl  12881  pcid  12899  pcneg  12900  pcgcd1  12903  pc2dvds  12905  pcprmpw2  12908  difsqpwdvds  12913  pcmpt  12918  pockthg  12932  1arith  12942  mul4sq  12969  4sqexercise2  12974  ennnfonelemg  13026  ennnfonelemex  13037  ennnfonelemrnh  13039  ennnfonelemrn  13042  ennnfonelemdm  13043  ennnfonelemnn0  13045  ennnfonelemim  13047  ennnfone  13048  ctinfomlemom  13050  ctinf  13053  ctiunctlemfo  13062  nninfdclemcl  13071  nninfdclemf  13072  nninfdclemp1  13073  unbendc  13077  isstruct2r  13095  setscom  13124  qusval  13408  ercpbl  13416  opifismgmdc  13456  grpinvalem  13470  grprida  13472  igsumvalx  13474  gsumfzval  13476  gsumpropd2  13478  gsumval2  13482  sgrppropd  13498  prdssgrpd  13500  mndpropd  13525  issubmnd  13527  submnd0  13529  prdsmndd  13533  mhmf1o  13555  0mhm  13571  resmhm  13572  mhmco  13575  mhmima  13576  mhmeql  13577  gsumwsubmcl  13581  gsumfzcl  13584  grppropd  13602  grpinvid1  13637  grpinvid2  13638  grplcan  13647  grplmulf1o  13659  grpnpncan0  13681  dfgrp3mlem  13683  grplactcnv  13687  pwssub  13698  mulgval  13711  mulgfng  13713  mulg1  13718  mulgnnp1  13719  mulgneg  13729  mulgnndir  13740  mulgdirlem  13742  mulgnn0ass  13747  mulgass  13748  subgmulg  13777  issubg4m  13782  subgintm  13787  0nsg  13803  eqgcpbl  13817  ghmmulg  13845  ghmpreima  13855  ghmeql  13856  ghmnsgima  13857  ghmnsgpreima  13858  ghmf1  13862  ghmf1o  13864  conjghm  13865  conjnmzb  13869  qusghm  13871  ablpncan3  13906  invghm  13918  eqgabl  13919  qusecsub  13920  gsumfzreidx  13926  gsumfzsubmcl  13927  gsumfzmptfidmadd  13928  gsumfzmhm  13932  imasrng  13972  qusrng  13974  srglmhm  14009  srgrmhm  14010  ringpropd  14054  ringlghm  14077  ringrghm  14078  imasring  14080  qusring2  14082  opprrngbg  14094  dvdsrvald  14110  dvdsrd  14111  dvdsrex  14115  dvdsrtr  14118  unitgrp  14133  unitpropdg  14165  rhmopp  14193  isnzr2  14201  issubrng2  14227  subrngintm  14229  subrgintm  14260  rhmpropd  14271  aprap  14303  lmodprop2d  14365  rmodislmodlem  14367  lssvacl  14382  lssvsubcl  14383  lssvscl  14392  islss3  14396  lsspropdg  14448  rnglidlmcl  14497  2idlcpblrng  14540  crngridl  14547  expghmap  14624  mulgghm2  14625  mulgrhm  14626  znf1o  14668  znleval  14670  znidom  14674  psrval  14683  mplsubgfilemcl  14716  epttop  14817  topssnei  14889  restbasg  14895  restopnb  14908  cnfval  14921  cnpfval  14922  iscnp4  14945  cnpnei  14946  cnptopco  14949  cncnp  14957  cnrest2  14963  cnptoprest  14966  cnptoprest2  14967  lmss  14973  lmtopcnp  14977  neitx  14995  txcnp  14998  txrest  15003  txdis  15004  txlm  15006  cnmpt21  15018  imasnopn  15026  xmetres2  15106  blvalps  15115  blval  15116  bl2in  15130  blhalf  15135  blssps  15154  blss  15155  blssexps  15156  blssex  15157  ssblex  15158  blin2  15159  metss2lem  15224  bdmetval  15227  bdmopn  15231  metrest  15233  xmetxp  15234  xmetxpbl  15235  xmettx  15237  metcnp3  15238  txmetcnp  15245  addcncntoplem  15288  elcncf2  15301  mulc1cncf  15316  cncfco  15318  cncfmet  15319  mulcncf  15335  dedekindeulemub  15345  dedekindeulemloc  15346  dedekindeulemlu  15348  dedekindeu  15350  suplociccex  15352  dedekindicclemub  15354  dedekindicclemloc  15355  dedekindicclemlu  15357  dedekindicc  15360  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthdec  15371  ivthreinc  15372  dich0  15379  limcimolemlt  15391  limcimo  15392  cnplimccntop  15397  limccnp2lem  15403  limccnp2cntop  15404  dvfvalap  15408  dvmptfsum  15452  dveflem  15453  plyco  15486  plycn  15489  plyrecj  15490  reeff1olem  15498  reeff1oleme  15499  eflt  15502  sin0pilem2  15509  pilem3  15510  ptolemy  15551  ioocosf1o  15581  cxplt  15643  cxple  15644  cxplt3  15647  apcxp2  15666  rprelogbmul  15682  rprelogbdiv  15684  logbgt0b  15693  logbgcd1irrap  15697  fsumdvdsmul  15718  perfectlem2  15727  lgsdir2lem5  15764  lgsdir  15767  lgsdi  15769  lgsne0  15770  gausslemma2dlem1f1o  15792  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2lem2  15814  lgsquad2  15815  2sqlem6  15852  2sqlem10  15857  upgredg  15998  uhgrissubgr  16115  subgrprop3  16116  upgrspanop  16137  umgrspanop  16138  usgrspanop  16139  vtxedgfi  16143  vtxlpfi  16144  upgr2wlkdc  16231  clwwlkccatlem  16254  eupth2lemsfi  16332  depindlem3  16348  nnti  16612  pwtrufal  16619  pwf1oexmid  16621  sssneq  16624  qdencn  16652  cvgcmp2n  16658  trilpolemlt1  16666  trirec0  16669  trirec0xor  16670  redc0  16682  reap0  16683  cndcap  16684  nconstwlpolemgt0  16689  neap0mkv  16694  supfz  16696  inffz  16697  gfsumval  16701  gfsumcl  16708