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  3135  elpr2elpr  3879  disjiun  4103  reg3exmidlemwe  4700  opabssxpd  4785  0xp  4829  imainss  5177  iotam  5343  fvmptt  5768  fcof1o  5961  isotr  5988  riota5f  6029  ovmpodf  6184  unielxp  6367  fnmpoovd  6410  1stconst  6416  2ndconst  6417  cnvf1olem  6419  fvn0elsupp  6450  suppcofn  6465  tfrlemi14d  6563  tfrexlem  6564  tfr1onlemres  6579  tfrcllemres  6592  tfrcldm  6593  frecabcl  6629  nnaordi  6740  swoer  6794  qliftfun  6850  ecopovsymg  6867  th3qlem1  6870  pw2f1odclem  7086  mapen  7098  mapxpen  7100  fidifsnen  7124  fisbth  7139  findcard2d  7147  findcard2sd  7148  diffisn  7149  diffifi  7150  ac6sfi  7154  fidcen  7155  fimax2gtri  7158  fientri3  7174  nnwetri  7175  unsnfi  7178  unsnfidcex  7179  unsnfidcel  7180  fisseneq  7194  exmidssfi  7198  fidcenumlemrk  7223  fidcenumlemr  7224  isbth  7236  ordiso2  7325  difinfsnlem  7389  difinfinf  7391  ctmlemr  7398  ctssdccl  7401  fodjum  7436  fodju0  7437  omniwomnimkv  7457  exmidfodomrlemrALT  7505  netap  7564  exmidmotap  7571  cc1  7575  cc2lem  7576  cc3  7578  cc4f  7579  cc4n  7581  dfplpq2  7665  dfmpq2  7666  mulpipqqs  7684  distrnqg  7698  ltexnqq  7719  subhalfnqq  7725  distrnq0  7770  prarloclemup  7806  prarloclem3  7808  prarloc  7814  genplt2i  7821  nqprl  7862  nqpru  7863  prmuloc  7877  mullocpr  7882  distrlem4prl  7895  distrlem4pru  7896  ltaddpr  7908  ltexprlemopl  7912  ltexprlemlol  7913  ltexprlemopu  7914  ltexprlemupu  7915  ltexprlemrl  7921  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  ltaprlem  7929  ltaprg  7930  prplnqu  7931  addextpr  7932  recexprlemdisj  7941  recexprlemloc  7942  recexprlem1ssl  7944  aptiprleml  7950  aptiprlemu  7951  ltmprr  7953  archpr  7954  cauappcvgprlemopl  7957  cauappcvgprlemopu  7959  cauappcvgprlemdisj  7962  cauappcvgprlemloc  7963  cauappcvgprlem1  7970  cauappcvgprlem2  7971  cauappcvgprlemlim  7972  caucvgprlemnkj  7977  caucvgprlemopl  7980  caucvgprlemopu  7982  caucvgprlemdisj  7985  caucvgprlemloc  7986  caucvgprlem2  7991  caucvgprprlemnkltj  8000  caucvgprprlemnkeqj  8001  caucvgprprlemnjltk  8002  caucvgprprlemmu  8006  caucvgprprlemopl  8008  caucvgprprlemopu  8010  caucvgprprlemdisj  8013  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  caucvgprprlemaddq  8019  caucvgprprlem2  8021  suplocexprlemrl  8028  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemex  8033  suplocexprlemub  8034  suplocexprlemlub  8035  recexgt0sr  8084  mulgt0sr  8089  prsrriota  8099  caucvgsrlemoffres  8111  suplocsrlem  8119  cnm  8143  addcnsr  8145  mulcnsr  8146  mulcnsrec  8154  axaddcl  8175  axmulcl  8177  axmulcom  8182  rereceu  8200  recriota  8201  axcaucvglemres  8210  axpre-suploclemres  8212  lelttr  8358  ltletr  8359  readdcan  8409  addcan  8449  addcan2  8450  addsub4  8512  ltadd2  8689  le2add  8714  lt2add  8715  lt2sub  8730  le2sub  8731  eqord1  8753  rimul  8855  rereim  8856  ltmul1  8862  apreim  8873  mulreim  8874  apcotr  8877  apadd1  8878  addext  8880  apneg  8881  mulext1  8882  mulext  8884  ltleap  8902  aprcl  8916  mulap0  8924  mulcanapd  8931  receuap  8939  recapb  8941  rec11ap  8980  rec11rap  8981  divdivdivap  8983  ddcanap  8996  divadddivap  8997  conjmulap  8999  subrecap  9109  prodgt0gt0  9121  prodge0  9124  ltmul12a  9130  lemulge11  9136  lt2mul2div  9149  ltrec  9153  lerec  9154  lt2msq  9156  lerec2  9159  le2msq  9171  msq11  9172  ledivp1  9173  mulle0r  9214  suprzclex  9672  peano5uzti  9682  supinfneg  9923  infsupneg  9924  qapne  9967  xrlelttr  10135  xrltletr  10136  xrre  10149  xaddge0  10207  xle2add  10208  xlt2add  10209  divelunit  10331  fzass4  10392  fzocatel  10540  zsupcllemstep  10585  zssinfcl  10588  suprzubdc  10592  zsupssdc  10594  suprzcl2dc  10595  exbtwnzlemex  10605  rebtwn2z  10610  qbtwnre  10612  modqid  10707  modqcyc  10717  modqaddabs  10720  modqaddmod  10721  mulqaddmodid  10722  modqadd2mod  10732  modqltm1p1mod  10734  modqsubmod  10740  modqsubmodmod  10741  modqmulmod  10747  modqmulmodr  10748  modqaddmulmod  10749  modqsubdir  10751  frec2uzisod  10765  iseqovex  10816  seqvalcd  10819  seq1g  10821  seqf  10822  seqovcd  10825  seqm1g  10832  seq3fveq2  10833  seq3shft2  10839  seqshft2g  10840  monoord  10843  seq3split  10846  seqsplitg  10847  iseqf1olemnab  10859  seqf1oglem1  10877  seqf1og  10879  seq3id2  10884  seqhomog  10888  seq3distr  10890  expcl2lemap  10909  expnegzap  10931  ltexp2a  10949  le2sq2  10973  nn0ltexp2  11067  nn0opth2  11082  bcval5  11121  hashcl  11139  hashen  11142  fihashdom  11162  hashunlem  11163  hashun  11164  fimaxq  11187  hashfibclem  11199  hashfibc  11200  zfz1isolem1  11205  zfz1iso  11206  lencl  11221  sswrd  11226  fstwrdne0  11257  lswlgt0cl  11270  ccatw2s1p1g  11326  ccat2s1fstg  11329  swrdval  11333  wrdind  11407  wrd2ind  11408  swrdccatfn  11409  swrdccatin1  11410  swrdccatin2  11414  pfxccatin12lem2  11416  pfxccatin12  11418  pfxccat3a  11423  reuccatpfxs1  11432  cvg1nlemres  11663  cvg1n  11664  recvguniq  11673  resqrexlemp1rp  11684  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemex  11703  sqrtmul  11713  sqrtsq  11722  absexpzap  11758  absle  11767  abs3lem  11789  amgm2  11796  maxleastlt  11893  maxltsup  11896  fimaxre2  11905  xrmaxleastlt  11934  xrmaxltsup  11936  xrmaxaddlem  11938  climcn2  11987  addcn2  11988  mulcn2  11990  reccn2ap  11991  climcau  12025  summodclem2  12061  summodc  12062  fsumf1o  12069  fisumss  12071  fsum3cvg3  12075  fsumcl2lem  12077  fsumadd  12085  fsum2dlemstep  12113  mptfzshft  12121  fsumrev  12122  fsummulc2  12127  modfsummod  12137  fsumrelem  12150  binom  12163  cvgratnn  12210  mertenslemub  12213  prodmodc  12257  zproddc  12258  fprodf1o  12267  fprodssdc  12269  fprodmul  12270  fprodrev  12298  fprod2dlemstep  12301  efcllem  12338  tanaddaplem  12417  dvdsval2  12469  moddvds  12478  dvdsabseq  12526  dvdsflip  12530  oexpneg  12556  fldivndvdslt  12616  bitsfi  12636  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemeu  12696  dfgcd3  12699  bezout  12700  dvdsmulgcd  12714  bezoutr  12721  nninfctlemfo  12729  ialgrlem1st  12732  lcmgcdlem  12767  coprmdvds2  12783  qredeu  12787  rpdvds  12789  isprm5lem  12831  isprm6  12837  pw2dvdslemn  12855  nonsq  12897  crth  12914  eulerthlemh  12921  pclemdc  12979  pcprendvds2  12982  pceu  12986  pcval  12987  pczpre  12988  pcmul  12992  pcqmul  12994  pcqcl  12997  pcid  13015  pcneg  13016  pcgcd1  13019  pc2dvds  13021  pcprmpw2  13024  difsqpwdvds  13029  pcmpt  13034  pockthg  13048  1arith  13058  mul4sq  13085  4sqexercise2  13090  ennnfonelemg  13143  ennnfonelemex  13154  ennnfonelemrnh  13156  ennnfonelemrn  13159  ennnfonelemdm  13160  ennnfonelemnn0  13162  ennnfonelemim  13164  ennnfone  13165  ctinfomlemom  13167  ctinf  13170  ctiunctlemfo  13179  nninfdclemcl  13188  nninfdclemf  13189  nninfdclemp1  13190  unbendc  13194  isstruct2r  13212  setscom  13241  qusval  13525  ercpbl  13533  opifismgmdc  13573  grpinvalem  13587  grprida  13589  igsumvalx  13591  gsumfzval  13593  gsumpropd2  13595  gsumval2  13599  sgrppropd  13615  prdssgrpd  13617  mndpropd  13642  issubmnd  13644  submnd0  13646  prdsmndd  13650  mhmf1o  13672  0mhm  13688  resmhm  13689  mhmco  13692  mhmima  13693  mhmeql  13694  gsumwsubmcl  13698  gsumfzcl  13701  grppropd  13719  grpinvid1  13754  grpinvid2  13755  grplcan  13764  grplmulf1o  13776  grpnpncan0  13798  dfgrp3mlem  13800  grplactcnv  13804  pwssub  13815  mulgval  13828  mulgfng  13830  mulg1  13835  mulgnnp1  13836  mulgneg  13846  mulgnndir  13857  mulgdirlem  13859  mulgnn0ass  13864  mulgass  13865  subgmulg  13894  issubg4m  13899  subgintm  13904  0nsg  13920  eqgcpbl  13934  ghmmulg  13962  ghmpreima  13972  ghmeql  13973  ghmnsgima  13974  ghmnsgpreima  13975  ghmf1  13979  ghmf1o  13981  conjghm  13982  conjnmzb  13986  qusghm  13988  ablpncan3  14023  invghm  14035  eqgabl  14036  qusecsub  14037  gsumfzreidx  14043  gsumfzsubmcl  14044  gsumfzmptfidmadd  14045  gsumfzmhm  14049  imasrng  14089  qusrng  14091  srglmhm  14126  srgrmhm  14127  ringpropd  14171  ringlghm  14194  ringrghm  14195  imasring  14197  qusring2  14199  opprrngbg  14211  dvdsrvald  14227  dvdsrd  14228  dvdsrex  14232  dvdsrtr  14235  unitgrp  14250  unitpropdg  14282  rhmopp  14310  isnzr2  14318  issubrng2  14344  subrngintm  14346  subrgintm  14377  rhmpropd  14388  aprap  14421  lmodprop2d  14483  rmodislmodlem  14485  lssvacl  14500  lssvsubcl  14501  lssvscl  14510  islss3  14514  lsspropdg  14566  rnglidlmcl  14615  2idlcpblrng  14658  crngridl  14665  expghmap  14742  mulgghm2  14743  mulgrhm  14744  znf1o  14786  znleval  14788  znidom  14792  psrval  14801  psrbagcon  14813  psrbagconf1o  14815  mplsubgfilemcl  14841  epttop  14942  topssnei  15014  restbasg  15020  restopnb  15033  cnfval  15046  cnpfval  15047  iscnp4  15070  cnpnei  15071  cnptopco  15074  cncnp  15082  cnrest2  15088  cnptoprest  15091  cnptoprest2  15092  lmss  15098  lmtopcnp  15102  neitx  15120  txcnp  15123  txrest  15128  txdis  15129  txlm  15131  cnmpt21  15143  imasnopn  15151  xmetres2  15231  blvalps  15240  blval  15241  bl2in  15255  blhalf  15260  blssps  15279  blss  15280  blssexps  15281  blssex  15282  ssblex  15283  blin2  15284  metss2lem  15349  bdmetval  15352  bdmopn  15356  metrest  15358  xmetxp  15359  xmetxpbl  15360  xmettx  15362  metcnp3  15363  txmetcnp  15370  addcncntoplem  15413  elcncf2  15426  mulc1cncf  15441  cncfco  15443  cncfmet  15444  mulcncf  15460  dedekindeulemub  15470  dedekindeulemloc  15471  dedekindeulemlu  15473  dedekindeu  15475  suplociccex  15477  dedekindicclemub  15479  dedekindicclemloc  15480  dedekindicclemlu  15482  dedekindicc  15485  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthdec  15496  ivthreinc  15497  dich0  15504  limcimolemlt  15516  limcimo  15517  cnplimccntop  15522  limccnp2lem  15528  limccnp2cntop  15529  dvfvalap  15533  dvmptfsum  15577  dveflem  15578  plyco  15611  plycn  15614  plyrecj  15615  reeff1olem  15623  reeff1oleme  15624  eflt  15627  sin0pilem2  15634  pilem3  15635  ptolemy  15676  ioocosf1o  15706  cxplt  15768  cxple  15769  cxplt3  15772  apcxp2  15791  rprelogbmul  15807  rprelogbdiv  15809  logbgt0b  15818  logbgcd1irrap  15822  pellexlem3  15834  fsumdvdsmul  15846  perfectlem2  15855  lgsdir2lem5  15892  lgsdir  15895  lgsdi  15897  lgsne0  15898  gausslemma2dlem1f1o  15920  lgseisenlem2  15931  lgsquadlem1  15937  lgsquadlem2  15938  lgsquad2lem2  15942  lgsquad2  15943  2sqlem6  15980  2sqlem10  15985  upgredg  16126  uhgrissubgr  16243  subgrprop3  16244  upgrspanop  16265  umgrspanop  16266  usgrspanop  16267  vtxedgfi  16271  vtxlpfi  16272  upgr2wlkdc  16359  clwwlkccatlem  16382  eupth2lemsfi  16460  depindlem3  16490  nnti  16753  pwtrufal  16758  pwf1oexmid  16760  sssneq  16763  qdencn  16794  cvgcmp2n  16804  trilpolemlt1  16812  trirec0  16815  trirec0xor  16816  qdiff  16820  redc0  16829  reap0  16830  cndcap  16831  nconstwlpolemgt0  16836  neap0mkv  16841  supfz  16843  inffz  16844  gfsumval  16848  gfsumcl  16856