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  3124  elpr2elpr  3860  disjiun  4084  reg3exmidlemwe  4679  opabssxpd  4764  0xp  4808  imainss  5154  iotam  5320  fvmptt  5741  fcof1o  5935  isotr  5962  riota5f  6003  ovmpodf  6158  unielxp  6342  fnmpoovd  6385  1stconst  6391  2ndconst  6392  cnvf1olem  6394  tfrlemi14d  6504  tfrexlem  6505  tfr1onlemres  6520  tfrcllemres  6533  tfrcldm  6534  frecabcl  6570  nnaordi  6681  swoer  6735  qliftfun  6791  ecopovsymg  6808  th3qlem1  6811  pw2f1odclem  7025  mapen  7037  mapxpen  7039  fidifsnen  7062  fisbth  7077  findcard2d  7085  findcard2sd  7086  diffisn  7087  diffifi  7088  ac6sfi  7092  fidcen  7093  fimax2gtri  7096  fientri3  7112  nnwetri  7113  unsnfi  7116  unsnfidcex  7117  unsnfidcel  7118  fisseneq  7132  exmidssfi  7136  fidcenumlemrk  7158  fidcenumlemr  7159  isbth  7171  ordiso2  7239  difinfsnlem  7303  difinfinf  7305  ctmlemr  7312  ctssdccl  7315  fodjum  7350  fodju0  7351  omniwomnimkv  7371  exmidfodomrlemrALT  7419  netap  7478  exmidmotap  7485  cc1  7489  cc2lem  7490  cc3  7492  cc4f  7493  cc4n  7495  dfplpq2  7579  dfmpq2  7580  mulpipqqs  7598  distrnqg  7612  ltexnqq  7633  subhalfnqq  7639  distrnq0  7684  prarloclemup  7720  prarloclem3  7722  prarloc  7728  genplt2i  7735  nqprl  7776  nqpru  7777  prmuloc  7791  mullocpr  7796  distrlem4prl  7809  distrlem4pru  7810  ltaddpr  7822  ltexprlemopl  7826  ltexprlemlol  7827  ltexprlemopu  7828  ltexprlemupu  7829  ltexprlemrl  7835  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  ltaprlem  7843  ltaprg  7844  prplnqu  7845  addextpr  7846  recexprlemdisj  7855  recexprlemloc  7856  recexprlem1ssl  7858  aptiprleml  7864  aptiprlemu  7865  ltmprr  7867  archpr  7868  cauappcvgprlemopl  7871  cauappcvgprlemopu  7873  cauappcvgprlemdisj  7876  cauappcvgprlemloc  7877  cauappcvgprlem1  7884  cauappcvgprlem2  7885  cauappcvgprlemlim  7886  caucvgprlemnkj  7891  caucvgprlemopl  7894  caucvgprlemopu  7896  caucvgprlemdisj  7899  caucvgprlemloc  7900  caucvgprlem2  7905  caucvgprprlemnkltj  7914  caucvgprprlemnkeqj  7915  caucvgprprlemnjltk  7916  caucvgprprlemmu  7920  caucvgprprlemopl  7922  caucvgprprlemopu  7924  caucvgprprlemdisj  7927  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  caucvgprprlemaddq  7933  caucvgprprlem2  7935  suplocexprlemrl  7942  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemex  7947  suplocexprlemub  7948  suplocexprlemlub  7949  recexgt0sr  7998  mulgt0sr  8003  prsrriota  8013  caucvgsrlemoffres  8025  suplocsrlem  8033  cnm  8057  addcnsr  8059  mulcnsr  8060  mulcnsrec  8068  axaddcl  8089  axmulcl  8091  axmulcom  8096  rereceu  8114  recriota  8115  axcaucvglemres  8124  axpre-suploclemres  8126  lelttr  8273  ltletr  8274  readdcan  8324  addcan  8364  addcan2  8365  addsub4  8427  ltadd2  8604  le2add  8629  lt2add  8630  lt2sub  8645  le2sub  8646  eqord1  8668  rimul  8770  rereim  8771  ltmul1  8777  apreim  8788  mulreim  8789  apcotr  8792  apadd1  8793  addext  8795  apneg  8796  mulext1  8797  mulext  8799  ltleap  8817  aprcl  8831  mulap0  8839  mulcanapd  8846  receuap  8854  recapb  8856  rec11ap  8895  rec11rap  8896  divdivdivap  8898  ddcanap  8911  divadddivap  8912  conjmulap  8914  subrecap  9024  prodgt0gt0  9036  prodge0  9039  ltmul12a  9045  lemulge11  9051  lt2mul2div  9064  ltrec  9068  lerec  9069  lt2msq  9071  lerec2  9074  le2msq  9086  msq11  9087  ledivp1  9088  mulle0r  9129  suprzclex  9583  peano5uzti  9593  supinfneg  9834  infsupneg  9835  qapne  9878  xrlelttr  10046  xrltletr  10047  xrre  10060  xaddge0  10118  xle2add  10119  xlt2add  10120  divelunit  10242  fzass4  10302  fzocatel  10450  zsupcllemstep  10495  zssinfcl  10498  suprzubdc  10502  zsupssdc  10504  suprzcl2dc  10505  exbtwnzlemex  10515  rebtwn2z  10520  qbtwnre  10522  modqid  10617  modqcyc  10627  modqaddabs  10630  modqaddmod  10631  mulqaddmodid  10632  modqadd2mod  10642  modqltm1p1mod  10644  modqsubmod  10650  modqsubmodmod  10651  modqmulmod  10657  modqmulmodr  10658  modqaddmulmod  10659  modqsubdir  10661  frec2uzisod  10675  iseqovex  10726  seqvalcd  10729  seq1g  10731  seqf  10732  seqovcd  10735  seqm1g  10742  seq3fveq2  10743  seq3shft2  10749  seqshft2g  10750  monoord  10753  seq3split  10756  seqsplitg  10757  iseqf1olemnab  10769  seqf1oglem1  10787  seqf1og  10789  seq3id2  10794  seqhomog  10798  seq3distr  10800  expcl2lemap  10819  expnegzap  10841  ltexp2a  10859  le2sq2  10883  nn0ltexp2  10977  nn0opth2  10992  bcval5  11031  hashcl  11049  hashen  11052  fihashdom  11072  hashunlem  11073  hashun  11074  fimaxq  11097  zfz1isolem1  11110  zfz1iso  11111  lencl  11126  sswrd  11131  fstwrdne0  11162  lswlgt0cl  11175  ccatw2s1p1g  11231  ccat2s1fstg  11234  swrdval  11238  wrdind  11312  wrd2ind  11313  swrdccatfn  11314  swrdccatin1  11315  swrdccatin2  11319  pfxccatin12lem2  11321  pfxccatin12  11323  pfxccat3a  11328  reuccatpfxs1  11337  cvg1nlemres  11568  cvg1n  11569  recvguniq  11578  resqrexlemp1rp  11589  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemex  11608  sqrtmul  11618  sqrtsq  11627  absexpzap  11663  absle  11672  abs3lem  11694  amgm2  11701  maxleastlt  11798  maxltsup  11801  fimaxre2  11810  xrmaxleastlt  11839  xrmaxltsup  11841  xrmaxaddlem  11843  climcn2  11892  addcn2  11893  mulcn2  11895  reccn2ap  11896  climcau  11930  summodclem2  11966  summodc  11967  fsumf1o  11974  fisumss  11976  fsum3cvg3  11980  fsumcl2lem  11982  fsumadd  11990  fsum2dlemstep  12018  mptfzshft  12026  fsumrev  12027  fsummulc2  12032  modfsummod  12042  fsumrelem  12055  binom  12068  cvgratnn  12115  mertenslemub  12118  prodmodc  12162  zproddc  12163  fprodf1o  12172  fprodssdc  12174  fprodmul  12175  fprodrev  12203  fprod2dlemstep  12206  efcllem  12243  tanaddaplem  12322  dvdsval2  12374  moddvds  12383  dvdsabseq  12431  dvdsflip  12435  oexpneg  12461  fldivndvdslt  12521  bitsfi  12541  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemeu  12601  dfgcd3  12604  bezout  12605  dvdsmulgcd  12619  bezoutr  12626  nninfctlemfo  12634  ialgrlem1st  12637  lcmgcdlem  12672  coprmdvds2  12688  qredeu  12692  rpdvds  12694  isprm5lem  12736  isprm6  12742  pw2dvdslemn  12760  nonsq  12802  crth  12819  eulerthlemh  12826  pclemdc  12884  pcprendvds2  12887  pceu  12891  pcval  12892  pczpre  12893  pcmul  12897  pcqmul  12899  pcqcl  12902  pcid  12920  pcneg  12921  pcgcd1  12924  pc2dvds  12926  pcprmpw2  12929  difsqpwdvds  12934  pcmpt  12939  pockthg  12953  1arith  12963  mul4sq  12990  4sqexercise2  12995  ennnfonelemg  13047  ennnfonelemex  13058  ennnfonelemrnh  13060  ennnfonelemrn  13063  ennnfonelemdm  13064  ennnfonelemnn0  13066  ennnfonelemim  13068  ennnfone  13069  ctinfomlemom  13071  ctinf  13074  ctiunctlemfo  13083  nninfdclemcl  13092  nninfdclemf  13093  nninfdclemp1  13094  unbendc  13098  isstruct2r  13116  setscom  13145  qusval  13429  ercpbl  13437  opifismgmdc  13477  grpinvalem  13491  grprida  13493  igsumvalx  13495  gsumfzval  13497  gsumpropd2  13499  gsumval2  13503  sgrppropd  13519  prdssgrpd  13521  mndpropd  13546  issubmnd  13548  submnd0  13550  prdsmndd  13554  mhmf1o  13576  0mhm  13592  resmhm  13593  mhmco  13596  mhmima  13597  mhmeql  13598  gsumwsubmcl  13602  gsumfzcl  13605  grppropd  13623  grpinvid1  13658  grpinvid2  13659  grplcan  13668  grplmulf1o  13680  grpnpncan0  13702  dfgrp3mlem  13704  grplactcnv  13708  pwssub  13719  mulgval  13732  mulgfng  13734  mulg1  13739  mulgnnp1  13740  mulgneg  13750  mulgnndir  13761  mulgdirlem  13763  mulgnn0ass  13768  mulgass  13769  subgmulg  13798  issubg4m  13803  subgintm  13808  0nsg  13824  eqgcpbl  13838  ghmmulg  13866  ghmpreima  13876  ghmeql  13877  ghmnsgima  13878  ghmnsgpreima  13879  ghmf1  13883  ghmf1o  13885  conjghm  13886  conjnmzb  13890  qusghm  13892  ablpncan3  13927  invghm  13939  eqgabl  13940  qusecsub  13941  gsumfzreidx  13947  gsumfzsubmcl  13948  gsumfzmptfidmadd  13949  gsumfzmhm  13953  imasrng  13993  qusrng  13995  srglmhm  14030  srgrmhm  14031  ringpropd  14075  ringlghm  14098  ringrghm  14099  imasring  14101  qusring2  14103  opprrngbg  14115  dvdsrvald  14131  dvdsrd  14132  dvdsrex  14136  dvdsrtr  14139  unitgrp  14154  unitpropdg  14186  rhmopp  14214  isnzr2  14222  issubrng2  14248  subrngintm  14250  subrgintm  14281  rhmpropd  14292  aprap  14324  lmodprop2d  14386  rmodislmodlem  14388  lssvacl  14403  lssvsubcl  14404  lssvscl  14413  islss3  14417  lsspropdg  14469  rnglidlmcl  14518  2idlcpblrng  14561  crngridl  14568  expghmap  14645  mulgghm2  14646  mulgrhm  14647  znf1o  14689  znleval  14691  znidom  14695  psrval  14704  psrbagcon  14714  psrbagconf1o  14716  mplsubgfilemcl  14742  epttop  14843  topssnei  14915  restbasg  14921  restopnb  14934  cnfval  14947  cnpfval  14948  iscnp4  14971  cnpnei  14972  cnptopco  14975  cncnp  14983  cnrest2  14989  cnptoprest  14992  cnptoprest2  14993  lmss  14999  lmtopcnp  15003  neitx  15021  txcnp  15024  txrest  15029  txdis  15030  txlm  15032  cnmpt21  15044  imasnopn  15052  xmetres2  15132  blvalps  15141  blval  15142  bl2in  15156  blhalf  15161  blssps  15180  blss  15181  blssexps  15182  blssex  15183  ssblex  15184  blin2  15185  metss2lem  15250  bdmetval  15253  bdmopn  15257  metrest  15259  xmetxp  15260  xmetxpbl  15261  xmettx  15263  metcnp3  15264  txmetcnp  15271  addcncntoplem  15314  elcncf2  15327  mulc1cncf  15342  cncfco  15344  cncfmet  15345  mulcncf  15361  dedekindeulemub  15371  dedekindeulemloc  15372  dedekindeulemlu  15374  dedekindeu  15376  suplociccex  15378  dedekindicclemub  15380  dedekindicclemloc  15381  dedekindicclemlu  15383  dedekindicc  15386  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthdec  15397  ivthreinc  15398  dich0  15405  limcimolemlt  15417  limcimo  15418  cnplimccntop  15423  limccnp2lem  15429  limccnp2cntop  15430  dvfvalap  15434  dvmptfsum  15478  dveflem  15479  plyco  15512  plycn  15515  plyrecj  15516  reeff1olem  15524  reeff1oleme  15525  eflt  15528  sin0pilem2  15535  pilem3  15536  ptolemy  15577  ioocosf1o  15607  cxplt  15669  cxple  15670  cxplt3  15673  apcxp2  15692  rprelogbmul  15708  rprelogbdiv  15710  logbgt0b  15719  logbgcd1irrap  15723  fsumdvdsmul  15744  perfectlem2  15753  lgsdir2lem5  15790  lgsdir  15793  lgsdi  15795  lgsne0  15796  gausslemma2dlem1f1o  15818  lgseisenlem2  15829  lgsquadlem1  15835  lgsquadlem2  15836  lgsquad2lem2  15840  lgsquad2  15841  2sqlem6  15878  2sqlem10  15883  upgredg  16024  uhgrissubgr  16141  subgrprop3  16142  upgrspanop  16163  umgrspanop  16164  usgrspanop  16165  vtxedgfi  16169  vtxlpfi  16170  upgr2wlkdc  16257  clwwlkccatlem  16280  eupth2lemsfi  16358  depindlem3  16388  nnti  16651  pwtrufal  16658  pwf1oexmid  16660  sssneq  16663  qdencn  16694  cvgcmp2n  16704  trilpolemlt1  16712  trirec0  16715  trirec0xor  16716  qdiff  16720  redc0  16729  reap0  16730  cndcap  16731  nconstwlpolemgt0  16736  neap0mkv  16741  supfz  16743  inffz  16744  gfsumval  16748  gfsumcl  16755