Theorem simprl 529

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  987  simp1rl  1086  simp2rl  1090  simp3rl  1094  rmob  3122  elpr2elpr  3854  disjiun  4078  reg3exmidlemwe  4672  opabssxpd  4757  0xp  4801  imainss  5147  iotam  5313  fvmptt  5731  fcof1o  5922  isotr  5949  riota5f  5990  ovmpodf  6145  unielxp  6329  fnmpoovd  6372  1stconst  6378  2ndconst  6379  cnvf1olem  6381  tfrlemi14d  6490  tfrexlem  6491  tfr1onlemres  6506  tfrcllemres  6519  tfrcldm  6520  frecabcl  6556  nnaordi  6667  swoer  6721  qliftfun  6777  ecopovsymg  6794  th3qlem1  6797  pw2f1odclem  7008  mapen  7020  mapxpen  7022  fidifsnen  7045  fisbth  7058  findcard2d  7066  findcard2sd  7067  diffisn  7068  diffifi  7069  ac6sfi  7073  fidcen  7074  fimax2gtri  7077  fientri3  7093  nnwetri  7094  unsnfi  7097  unsnfidcex  7098  unsnfidcel  7099  fisseneq  7112  fidcenumlemrk  7137  fidcenumlemr  7138  isbth  7150  ordiso2  7218  difinfsnlem  7282  difinfinf  7284  ctmlemr  7291  ctssdccl  7294  fodjum  7329  fodju0  7330  omniwomnimkv  7350  exmidfodomrlemrALT  7397  netap  7456  exmidmotap  7463  cc1  7467  cc2lem  7468  cc3  7470  cc4f  7471  cc4n  7473  dfplpq2  7557  dfmpq2  7558  mulpipqqs  7576  distrnqg  7590  ltexnqq  7611  subhalfnqq  7617  distrnq0  7662  prarloclemup  7698  prarloclem3  7700  prarloc  7706  genplt2i  7713  nqprl  7754  nqpru  7755  prmuloc  7769  mullocpr  7774  distrlem4prl  7787  distrlem4pru  7788  ltaddpr  7800  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  ltaprlem  7821  ltaprg  7822  prplnqu  7823  addextpr  7824  recexprlemdisj  7833  recexprlemloc  7834  recexprlem1ssl  7836  aptiprleml  7842  aptiprlemu  7843  ltmprr  7845  archpr  7846  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlem1  7862  cauappcvgprlem2  7863  cauappcvgprlemlim  7864  caucvgprlemnkj  7869  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlem2  7883  caucvgprprlemnkltj  7892  caucvgprprlemnkeqj  7893  caucvgprprlemnjltk  7894  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemopu  7902  caucvgprprlemdisj  7905  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlemaddq  7911  caucvgprprlem2  7913  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemex  7925  suplocexprlemub  7926  suplocexprlemlub  7927  recexgt0sr  7976  mulgt0sr  7981  prsrriota  7991  caucvgsrlemoffres  8003  suplocsrlem  8011  cnm  8035  addcnsr  8037  mulcnsr  8038  mulcnsrec  8046  axaddcl  8067  axmulcl  8069  axmulcom  8074  rereceu  8092  recriota  8093  axcaucvglemres  8102  axpre-suploclemres  8104  lelttr  8251  ltletr  8252  readdcan  8302  addcan  8342  addcan2  8343  addsub4  8405  ltadd2  8582  le2add  8607  lt2add  8608  lt2sub  8623  le2sub  8624  eqord1  8646  rimul  8748  rereim  8749  ltmul1  8755  apreim  8766  mulreim  8767  apcotr  8770  apadd1  8771  addext  8773  apneg  8774  mulext1  8775  mulext  8777  ltleap  8795  aprcl  8809  mulap0  8817  mulcanapd  8824  receuap  8832  recapb  8834  rec11ap  8873  rec11rap  8874  divdivdivap  8876  ddcanap  8889  divadddivap  8890  conjmulap  8892  subrecap  9002  prodgt0gt0  9014  prodge0  9017  ltmul12a  9023  lemulge11  9029  lt2mul2div  9042  ltrec  9046  lerec  9047  lt2msq  9049  lerec2  9052  le2msq  9064  msq11  9065  ledivp1  9066  mulle0r  9107  suprzclex  9561  peano5uzti  9571  supinfneg  9807  infsupneg  9808  qapne  9851  xrlelttr  10019  xrltletr  10020  xrre  10033  xaddge0  10091  xle2add  10092  xlt2add  10093  divelunit  10215  fzass4  10275  fzocatel  10422  zsupcllemstep  10466  zssinfcl  10469  suprzubdc  10473  zsupssdc  10475  suprzcl2dc  10476  exbtwnzlemex  10486  rebtwn2z  10491  qbtwnre  10493  modqid  10588  modqcyc  10598  modqaddabs  10601  modqaddmod  10602  mulqaddmodid  10603  modqadd2mod  10613  modqltm1p1mod  10615  modqsubmod  10621  modqsubmodmod  10622  modqmulmod  10628  modqmulmodr  10629  modqaddmulmod  10630  modqsubdir  10632  frec2uzisod  10646  iseqovex  10697  seqvalcd  10700  seq1g  10702  seqf  10703  seqovcd  10706  seqm1g  10713  seq3fveq2  10714  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  iseqf1olemnab  10740  seqf1oglem1  10758  seqf1og  10760  seq3id2  10765  seqhomog  10769  seq3distr  10771  expcl2lemap  10790  expnegzap  10812  ltexp2a  10830  le2sq2  10854  nn0ltexp2  10948  nn0opth2  10963  bcval5  11002  hashcl  11020  hashen  11023  fihashdom  11042  hashunlem  11043  hashun  11044  fimaxq  11067  zfz1isolem1  11080  zfz1iso  11081  lencl  11093  sswrd  11098  fstwrdne0  11129  lswlgt0cl  11142  swrdval  11201  wrdind  11275  wrd2ind  11276  swrdccatfn  11277  swrdccatin1  11278  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12  11286  pfxccat3a  11291  reuccatpfxs1  11300  cvg1nlemres  11517  cvg1n  11518  recvguniq  11527  resqrexlemp1rp  11538  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemex  11557  sqrtmul  11567  sqrtsq  11576  absexpzap  11612  absle  11621  abs3lem  11643  amgm2  11650  maxleastlt  11747  maxltsup  11750  fimaxre2  11759  xrmaxleastlt  11788  xrmaxltsup  11790  xrmaxaddlem  11792  climcn2  11841  addcn2  11842  mulcn2  11844  reccn2ap  11845  climcau  11879  summodclem2  11914  summodc  11915  fsumf1o  11922  fisumss  11924  fsum3cvg3  11928  fsumcl2lem  11930  fsumadd  11938  fsum2dlemstep  11966  mptfzshft  11974  fsumrev  11975  fsummulc2  11980  modfsummod  11990  fsumrelem  12003  binom  12016  cvgratnn  12063  mertenslemub  12066  prodmodc  12110  zproddc  12111  fprodf1o  12120  fprodssdc  12122  fprodmul  12123  fprodrev  12151  fprod2dlemstep  12154  efcllem  12191  tanaddaplem  12270  dvdsval2  12322  moddvds  12331  dvdsabseq  12379  dvdsflip  12383  oexpneg  12409  fldivndvdslt  12469  bitsfi  12489  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemeu  12549  dfgcd3  12552  bezout  12553  dvdsmulgcd  12567  bezoutr  12574  nninfctlemfo  12582  ialgrlem1st  12585  lcmgcdlem  12620  coprmdvds2  12636  qredeu  12640  rpdvds  12642  isprm5lem  12684  isprm6  12690  pw2dvdslemn  12708  nonsq  12750  crth  12767  eulerthlemh  12774  pclemdc  12832  pcprendvds2  12835  pceu  12839  pcval  12840  pczpre  12841  pcmul  12845  pcqmul  12847  pcqcl  12850  pcid  12868  pcneg  12869  pcgcd1  12872  pc2dvds  12874  pcprmpw2  12877  difsqpwdvds  12882  pcmpt  12887  pockthg  12901  1arith  12911  mul4sq  12938  4sqexercise2  12943  ennnfonelemg  12995  ennnfonelemex  13006  ennnfonelemrnh  13008  ennnfonelemrn  13011  ennnfonelemdm  13012  ennnfonelemnn0  13014  ennnfonelemim  13016  ennnfone  13017  ctinfomlemom  13019  ctinf  13022  ctiunctlemfo  13031  nninfdclemcl  13040  nninfdclemf  13041  nninfdclemp1  13042  unbendc  13046  isstruct2r  13064  setscom  13093  qusval  13377  ercpbl  13385  opifismgmdc  13425  grpinvalem  13439  grprida  13441  igsumvalx  13443  gsumfzval  13445  gsumpropd2  13447  gsumval2  13451  sgrppropd  13467  prdssgrpd  13469  mndpropd  13494  issubmnd  13496  submnd0  13498  prdsmndd  13502  mhmf1o  13524  0mhm  13540  resmhm  13541  mhmco  13544  mhmima  13545  mhmeql  13546  gsumwsubmcl  13550  gsumfzcl  13553  grppropd  13571  grpinvid1  13606  grpinvid2  13607  grplcan  13616  grplmulf1o  13628  grpnpncan0  13650  dfgrp3mlem  13652  grplactcnv  13656  pwssub  13667  mulgval  13680  mulgfng  13682  mulg1  13687  mulgnnp1  13688  mulgneg  13698  mulgnndir  13709  mulgdirlem  13711  mulgnn0ass  13716  mulgass  13717  subgmulg  13746  issubg4m  13751  subgintm  13756  0nsg  13772  eqgcpbl  13786  ghmmulg  13814  ghmpreima  13824  ghmeql  13825  ghmnsgima  13826  ghmnsgpreima  13827  ghmf1  13831  ghmf1o  13833  conjghm  13834  conjnmzb  13838  qusghm  13840  ablpncan3  13875  invghm  13887  eqgabl  13888  qusecsub  13889  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  imasrng  13940  qusrng  13942  srglmhm  13977  srgrmhm  13978  ringpropd  14022  ringlghm  14045  ringrghm  14046  imasring  14048  qusring2  14050  opprrngbg  14062  dvdsrvald  14078  dvdsrd  14079  dvdsrex  14083  dvdsrtr  14086  unitgrp  14101  unitpropdg  14133  rhmopp  14161  isnzr2  14169  issubrng2  14195  subrngintm  14197  subrgintm  14228  rhmpropd  14239  aprap  14271  lmodprop2d  14333  rmodislmodlem  14335  lssvacl  14350  lssvsubcl  14351  lssvscl  14360  islss3  14364  lsspropdg  14416  rnglidlmcl  14465  2idlcpblrng  14508  crngridl  14515  expghmap  14592  mulgghm2  14593  mulgrhm  14594  znf1o  14636  znleval  14638  znidom  14642  psrval  14651  mplsubgfilemcl  14684  epttop  14785  topssnei  14857  restbasg  14863  restopnb  14876  cnfval  14889  cnpfval  14890  iscnp4  14913  cnpnei  14914  cnptopco  14917  cncnp  14925  cnrest2  14931  cnptoprest  14934  cnptoprest2  14935  lmss  14941  lmtopcnp  14945  neitx  14963  txcnp  14966  txrest  14971  txdis  14972  txlm  14974  cnmpt21  14986  imasnopn  14994  xmetres2  15074  blvalps  15083  blval  15084  bl2in  15098  blhalf  15103  blssps  15122  blss  15123  blssexps  15124  blssex  15125  ssblex  15126  blin2  15127  metss2lem  15192  bdmetval  15195  bdmopn  15199  metrest  15201  xmetxp  15202  xmetxpbl  15203  xmettx  15205  metcnp3  15206  txmetcnp  15213  addcncntoplem  15256  elcncf2  15269  mulc1cncf  15284  cncfco  15286  cncfmet  15287  mulcncf  15303  dedekindeulemub  15313  dedekindeulemloc  15314  dedekindeulemlu  15316  dedekindeu  15318  suplociccex  15320  dedekindicclemub  15322  dedekindicclemloc  15323  dedekindicclemlu  15325  dedekindicc  15328  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthdec  15339  ivthreinc  15340  dich0  15347  limcimolemlt  15359  limcimo  15360  cnplimccntop  15365  limccnp2lem  15371  limccnp2cntop  15372  dvfvalap  15376  dvmptfsum  15420  dveflem  15421  plyco  15454  plycn  15457  plyrecj  15458  reeff1olem  15466  reeff1oleme  15467  eflt  15470  sin0pilem2  15477  pilem3  15478  ptolemy  15519  ioocosf1o  15549  cxplt  15611  cxple  15612  cxplt3  15615  apcxp2  15634  rprelogbmul  15650  rprelogbdiv  15652  logbgt0b  15661  logbgcd1irrap  15665  fsumdvdsmul  15686  perfectlem2  15695  lgsdir2lem5  15732  lgsdir  15735  lgsdi  15737  lgsne0  15738  gausslemma2dlem1f1o  15760  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem2  15782  lgsquad2  15783  2sqlem6  15820  2sqlem10  15825  upgredg  15963  vtxedgfi  16075  vtxlpfi  16076  upgr2wlkdc  16147  clwwlkccatlem  16169  nnti  16469  pwtrufal  16476  pwf1oexmid  16478  sssneq  16481  qdencn  16509  cvgcmp2n  16515  trilpolemlt1  16523  trirec0  16526  trirec0xor  16527  redc0  16539  reap0  16540  cndcap  16541  nconstwlpolemgt0  16546  neap0mkv  16551  supfz  16553  inffz  16554