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  7567  exmidmotap  7574  cc1  7578  cc2lem  7579  cc3  7581  cc4f  7582  cc4n  7584  dfplpq2  7668  dfmpq2  7669  mulpipqqs  7687  distrnqg  7701  ltexnqq  7722  subhalfnqq  7728  distrnq0  7773  prarloclemup  7809  prarloclem3  7811  prarloc  7817  genplt2i  7824  nqprl  7865  nqpru  7866  prmuloc  7880  mullocpr  7885  distrlem4prl  7898  distrlem4pru  7899  ltaddpr  7911  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemrl  7924  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  ltaprlem  7932  ltaprg  7933  prplnqu  7934  addextpr  7935  recexprlemdisj  7944  recexprlemloc  7945  recexprlem1ssl  7947  aptiprleml  7953  aptiprlemu  7954  ltmprr  7956  archpr  7957  cauappcvgprlemopl  7960  cauappcvgprlemopu  7962  cauappcvgprlemdisj  7965  cauappcvgprlemloc  7966  cauappcvgprlem1  7973  cauappcvgprlem2  7974  cauappcvgprlemlim  7975  caucvgprlemnkj  7980  caucvgprlemopl  7983  caucvgprlemopu  7985  caucvgprlemdisj  7988  caucvgprlemloc  7989  caucvgprlem2  7994  caucvgprprlemnkltj  8003  caucvgprprlemnkeqj  8004  caucvgprprlemnjltk  8005  caucvgprprlemmu  8009  caucvgprprlemopl  8011  caucvgprprlemopu  8013  caucvgprprlemdisj  8016  caucvgprprlemloc  8017  caucvgprprlemexbt  8020  caucvgprprlemaddq  8022  caucvgprprlem2  8024  suplocexprlemrl  8031  suplocexprlemmu  8032  suplocexprlemru  8033  suplocexprlemdisj  8034  suplocexprlemloc  8035  suplocexprlemex  8036  suplocexprlemub  8037  suplocexprlemlub  8038  recexgt0sr  8087  mulgt0sr  8092  prsrriota  8102  caucvgsrlemoffres  8114  suplocsrlem  8122  cnm  8146  addcnsr  8148  mulcnsr  8149  mulcnsrec  8157  axaddcl  8178  axmulcl  8180  axmulcom  8185  rereceu  8203  recriota  8204  axcaucvglemres  8213  axpre-suploclemres  8215  lelttr  8361  ltletr  8362  readdcan  8412  addcan  8452  addcan2  8453  addsub4  8515  ltadd2  8692  le2add  8717  lt2add  8718  lt2sub  8733  le2sub  8734  eqord1  8756  rimul  8858  rereim  8859  ltmul1  8865  apreim  8876  mulreim  8877  apcotr  8880  apadd1  8881  addext  8883  apneg  8884  mulext1  8885  mulext  8887  ltleap  8905  aprcl  8919  mulap0  8927  mulcanapd  8934  receuap  8942  recapb  8944  rec11ap  8983  rec11rap  8984  divdivdivap  8986  ddcanap  8999  divadddivap  9000  conjmulap  9002  subrecap  9112  prodgt0gt0  9124  prodge0  9127  ltmul12a  9133  lemulge11  9139  lt2mul2div  9152  ltrec  9156  lerec  9157  lt2msq  9159  lerec2  9162  le2msq  9174  msq11  9175  ledivp1  9176  mulle0r  9217  suprzclex  9675  peano5uzti  9685  supinfneg  9926  infsupneg  9927  qapne  9970  xrlelttr  10138  xrltletr  10139  xrre  10152  xaddge0  10210  xle2add  10211  xlt2add  10212  divelunit  10334  fzass4  10395  fzocatel  10543  zsupcllemstep  10588  zssinfcl  10591  suprzubdc  10595  zsupssdc  10597  suprzcl2dc  10598  exbtwnzlemex  10608  rebtwn2z  10613  qbtwnre  10615  modqid  10710  modqcyc  10720  modqaddabs  10723  modqaddmod  10724  mulqaddmodid  10725  modqadd2mod  10735  modqltm1p1mod  10737  modqsubmod  10743  modqsubmodmod  10744  modqmulmod  10750  modqmulmodr  10751  modqaddmulmod  10752  modqsubdir  10754  frec2uzisod  10768  iseqovex  10819  seqvalcd  10822  seq1g  10824  seqf  10825  seqovcd  10828  seqm1g  10835  seq3fveq2  10836  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  iseqf1olemnab  10862  seqf1oglem1  10880  seqf1og  10882  seq3id2  10887  seqhomog  10891  seq3distr  10893  expcl2lemap  10912  expnegzap  10934  ltexp2a  10952  le2sq2  10976  nn0ltexp2  11070  nn0opth2  11085  bcval5  11124  hashcl  11142  hashen  11145  fihashdom  11165  hashunlem  11166  hashun  11167  fimaxq  11190  hashfibclem  11202  hashfibc  11203  zfz1isolem1  11208  zfz1iso  11209  lencl  11224  sswrd  11229  fstwrdne0  11260  lswlgt0cl  11273  ccatw2s1p1g  11329  ccat2s1fstg  11332  swrdval  11336  wrdind  11410  wrd2ind  11411  swrdccatfn  11412  swrdccatin1  11413  swrdccatin2  11417  pfxccatin12lem2  11419  pfxccatin12  11421  pfxccat3a  11426  reuccatpfxs1  11435  cvg1nlemres  11666  cvg1n  11667  recvguniq  11676  resqrexlemp1rp  11687  resqrexlemoverl  11702  resqrexlemglsq  11703  resqrexlemex  11706  sqrtmul  11716  sqrtsq  11725  absexpzap  11761  absle  11770  abs3lem  11792  amgm2  11799  maxleastlt  11896  maxltsup  11899  fimaxre2  11908  xrmaxleastlt  11937  xrmaxltsup  11939  xrmaxaddlem  11941  climcn2  11990  addcn2  11991  mulcn2  11993  reccn2ap  11994  climcau  12028  summodclem2  12064  summodc  12065  fsumf1o  12072  fisumss  12074  fsum3cvg3  12078  fsumcl2lem  12080  fsumadd  12088  fsum2dlemstep  12116  mptfzshft  12124  fsumrev  12125  fsummulc2  12130  modfsummod  12140  fsumrelem  12153  binom  12166  cvgratnn  12213  mertenslemub  12216  prodmodc  12260  zproddc  12261  fprodf1o  12270  fprodssdc  12272  fprodmul  12273  fprodrev  12301  fprod2dlemstep  12304  efcllem  12341  tanaddaplem  12420  dvdsval2  12472  moddvds  12481  dvdsabseq  12529  dvdsflip  12533  oexpneg  12559  fldivndvdslt  12619  bitsfi  12639  bezoutlemnewy  12688  bezoutlemstep  12689  bezoutlemeu  12699  dfgcd3  12702  bezout  12703  dvdsmulgcd  12717  bezoutr  12724  nninfctlemfo  12732  ialgrlem1st  12735  lcmgcdlem  12770  coprmdvds2  12786  qredeu  12790  rpdvds  12792  isprm5lem  12834  isprm6  12840  pw2dvdslemn  12858  nonsq  12900  crth  12917  eulerthlemh  12924  pclemdc  12982  pcprendvds2  12985  pceu  12989  pcval  12990  pczpre  12991  pcmul  12995  pcqmul  12997  pcqcl  13000  pcid  13018  pcneg  13019  pcgcd1  13022  pc2dvds  13024  pcprmpw2  13027  difsqpwdvds  13032  pcmpt  13037  pockthg  13051  1arith  13061  mul4sq  13088  4sqexercise2  13093  ennnfonelemg  13146  ennnfonelemex  13157  ennnfonelemrnh  13159  ennnfonelemrn  13162  ennnfonelemdm  13163  ennnfonelemnn0  13165  ennnfonelemim  13167  ennnfone  13168  ctinfomlemom  13170  ctinf  13173  ctiunctlemfo  13182  nninfdclemcl  13191  nninfdclemf  13192  nninfdclemp1  13193  unbendc  13197  isstruct2r  13215  setscom  13244  qusval  13528  ercpbl  13536  opifismgmdc  13576  grpinvalem  13590  grprida  13592  igsumvalx  13594  gsumfzval  13596  gsumpropd2  13598  gsumval2  13602  sgrppropd  13618  prdssgrpd  13620  mndpropd  13645  issubmnd  13647  submnd0  13649  prdsmndd  13653  mhmf1o  13675  0mhm  13691  resmhm  13692  mhmco  13695  mhmima  13696  mhmeql  13697  gsumwsubmcl  13701  gsumfzcl  13704  grppropd  13722  grpinvid1  13757  grpinvid2  13758  grplcan  13767  grplmulf1o  13779  grpnpncan0  13801  dfgrp3mlem  13803  grplactcnv  13807  pwssub  13818  mulgval  13831  mulgfng  13833  mulg1  13838  mulgnnp1  13839  mulgneg  13849  mulgnndir  13860  mulgdirlem  13862  mulgnn0ass  13867  mulgass  13868  subgmulg  13897  issubg4m  13902  subgintm  13907  0nsg  13923  eqgcpbl  13937  ghmmulg  13965  ghmpreima  13975  ghmeql  13976  ghmnsgima  13977  ghmnsgpreima  13978  ghmf1  13982  ghmf1o  13984  conjghm  13985  conjnmzb  13989  qusghm  13991  ablpncan3  14026  invghm  14038  eqgabl  14039  qusecsub  14040  gsumfzreidx  14046  gsumfzsubmcl  14047  gsumfzmptfidmadd  14048  gsumfzmhm  14052  imasrng  14092  qusrng  14094  srglmhm  14129  srgrmhm  14130  ringpropd  14174  ringlghm  14197  ringrghm  14198  imasring  14200  qusring2  14202  opprrngbg  14214  dvdsrvald  14230  dvdsrd  14231  dvdsrex  14235  dvdsrtr  14238  unitgrp  14253  unitpropdg  14285  rhmopp  14313  isnzr2  14321  issubrng2  14347  subrngintm  14349  subrgintm  14380  rhmpropd  14391  aprap  14424  lmodprop2d  14488  rmodislmodlem  14490  lssvacl  14505  lssvsubcl  14506  lssvscl  14515  islss3  14519  lsspropdg  14571  rnglidlmcl  14620  2idlcpblrng  14663  crngridl  14670  expghmap  14747  mulgghm2  14748  mulgrhm  14749  znf1o  14791  znleval  14793  znidom  14797  psrval  14806  psrbagcon  14818  psrbagconf1o  14820  mplsubgfilemcl  14846  epttop  14947  topssnei  15019  restbasg  15025  restopnb  15038  cnfval  15051  cnpfval  15052  iscnp4  15075  cnpnei  15076  cnptopco  15079  cncnp  15087  cnrest2  15093  cnptoprest  15096  cnptoprest2  15097  lmss  15103  lmtopcnp  15107  neitx  15125  txcnp  15128  txrest  15133  txdis  15134  txlm  15136  cnmpt21  15148  imasnopn  15156  xmetres2  15236  blvalps  15245  blval  15246  bl2in  15260  blhalf  15265  blssps  15284  blss  15285  blssexps  15286  blssex  15287  ssblex  15288  blin2  15289  metss2lem  15354  bdmetval  15357  bdmopn  15361  metrest  15363  xmetxp  15364  xmetxpbl  15365  xmettx  15367  metcnp3  15368  txmetcnp  15375  addcncntoplem  15418  elcncf2  15431  mulc1cncf  15446  cncfco  15448  cncfmet  15449  mulcncf  15465  dedekindeulemub  15475  dedekindeulemloc  15476  dedekindeulemlu  15478  dedekindeu  15480  suplociccex  15482  dedekindicclemub  15484  dedekindicclemloc  15485  dedekindicclemlu  15487  dedekindicc  15490  ivthinclemlopn  15493  ivthinclemuopn  15495  ivthdec  15501  ivthreinc  15502  dich0  15509  limcimolemlt  15521  limcimo  15522  cnplimccntop  15527  limccnp2lem  15533  limccnp2cntop  15534  dvfvalap  15538  dvmptfsum  15582  dveflem  15583  plyco  15616  plycn  15619  plyrecj  15620  reeff1olem  15628  reeff1oleme  15629  eflt  15632  sin0pilem2  15639  pilem3  15640  ptolemy  15681  ioocosf1o  15711  cxplt  15773  cxple  15774  cxplt3  15777  apcxp2  15796  rprelogbmul  15812  rprelogbdiv  15814  logbgt0b  15823  logbgcd1irrap  15827  pellexlem3  15839  fsumdvdsmul  15851  perfectlem2  15860  lgsdir2lem5  15897  lgsdir  15900  lgsdi  15902  lgsne0  15903  gausslemma2dlem1f1o  15925  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2lem2  15947  lgsquad2  15948  2sqlem6  15985  2sqlem10  15990  upgredg  16131  uhgrissubgr  16248  subgrprop3  16249  upgrspanop  16270  umgrspanop  16271  usgrspanop  16272  vtxedgfi  16276  vtxlpfi  16277  upgr2wlkdc  16364  clwwlkccatlem  16387  eupth2lemsfi  16465  depindlem3  16495  nnti  16758  pwtrufal  16763  pwf1oexmid  16765  sssneq  16768  qdencn  16799  cvgcmp2n  16809  trilpolemlt1  16817  trirec0  16820  trirec0xor  16821  qdiff  16825  redc0  16834  reap0  16835  cndcap  16836  nconstwlpolemgt0  16841  neap0mkv  16846  supfz  16848  inffz  16849  gfsumval  16853  gfsumcl  16861