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:  simp1rl  1065  simp2rl  1069  simp3rl  1073  rmob  3092  disjiun  4042  reg3exmidlemwe  4631  0xp  4759  imainss  5103  iotam  5268  fvmptt  5678  fcof1o  5865  isotr  5892  riota5f  5931  ovmpodf  6084  unielxp  6267  fnmpoovd  6308  1stconst  6314  2ndconst  6315  cnvf1olem  6317  tfrlemi14d  6426  tfrexlem  6427  tfr1onlemres  6442  tfrcllemres  6455  tfrcldm  6456  frecabcl  6492  nnaordi  6601  swoer  6655  qliftfun  6711  ecopovsymg  6728  th3qlem1  6731  pw2f1odclem  6938  mapen  6950  mapxpen  6952  fidifsnen  6974  fisbth  6987  findcard2d  6995  findcard2sd  6996  diffisn  6997  diffifi  6998  ac6sfi  7002  fimax2gtri  7005  fientri3  7019  nnwetri  7020  unsnfi  7023  unsnfidcex  7024  unsnfidcel  7025  fisseneq  7038  fidcenumlemrk  7063  fidcenumlemr  7064  isbth  7076  ordiso2  7144  difinfsnlem  7208  difinfinf  7210  ctmlemr  7217  ctssdccl  7220  fodjum  7255  fodju0  7256  omniwomnimkv  7276  exmidfodomrlemrALT  7318  netap  7373  exmidmotap  7380  cc1  7384  cc2lem  7385  cc3  7387  cc4f  7388  cc4n  7390  dfplpq2  7474  dfmpq2  7475  mulpipqqs  7493  distrnqg  7507  ltexnqq  7528  subhalfnqq  7534  distrnq0  7579  prarloclemup  7615  prarloclem3  7617  prarloc  7623  genplt2i  7630  nqprl  7671  nqpru  7672  prmuloc  7686  mullocpr  7691  distrlem4prl  7704  distrlem4pru  7705  ltaddpr  7717  ltexprlemopl  7721  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemrl  7730  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  ltaprlem  7738  ltaprg  7739  prplnqu  7740  addextpr  7741  recexprlemdisj  7750  recexprlemloc  7751  recexprlem1ssl  7753  aptiprleml  7759  aptiprlemu  7760  ltmprr  7762  archpr  7763  cauappcvgprlemopl  7766  cauappcvgprlemopu  7768  cauappcvgprlemdisj  7771  cauappcvgprlemloc  7772  cauappcvgprlem1  7779  cauappcvgprlem2  7780  cauappcvgprlemlim  7781  caucvgprlemnkj  7786  caucvgprlemopl  7789  caucvgprlemopu  7791  caucvgprlemdisj  7794  caucvgprlemloc  7795  caucvgprlem2  7800  caucvgprprlemnkltj  7809  caucvgprprlemnkeqj  7810  caucvgprprlemnjltk  7811  caucvgprprlemmu  7815  caucvgprprlemopl  7817  caucvgprprlemopu  7819  caucvgprprlemdisj  7822  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  caucvgprprlemaddq  7828  caucvgprprlem2  7830  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemex  7842  suplocexprlemub  7843  suplocexprlemlub  7844  recexgt0sr  7893  mulgt0sr  7898  prsrriota  7908  caucvgsrlemoffres  7920  suplocsrlem  7928  cnm  7952  addcnsr  7954  mulcnsr  7955  mulcnsrec  7963  axaddcl  7984  axmulcl  7986  axmulcom  7991  rereceu  8009  recriota  8010  axcaucvglemres  8019  axpre-suploclemres  8021  lelttr  8168  ltletr  8169  readdcan  8219  addcan  8259  addcan2  8260  addsub4  8322  ltadd2  8499  le2add  8524  lt2add  8525  lt2sub  8540  le2sub  8541  eqord1  8563  rimul  8665  rereim  8666  ltmul1  8672  apreim  8683  mulreim  8684  apcotr  8687  apadd1  8688  addext  8690  apneg  8691  mulext1  8692  mulext  8694  ltleap  8712  aprcl  8726  mulap0  8734  mulcanapd  8741  receuap  8749  recapb  8751  rec11ap  8790  rec11rap  8791  divdivdivap  8793  ddcanap  8806  divadddivap  8807  conjmulap  8809  subrecap  8919  prodgt0gt0  8931  prodge0  8934  ltmul12a  8940  lemulge11  8946  lt2mul2div  8959  ltrec  8963  lerec  8964  lt2msq  8966  lerec2  8969  le2msq  8981  msq11  8982  ledivp1  8983  mulle0r  9024  suprzclex  9478  peano5uzti  9488  supinfneg  9723  infsupneg  9724  qapne  9767  xrlelttr  9935  xrltletr  9936  xrre  9949  xaddge0  10007  xle2add  10008  xlt2add  10009  divelunit  10131  fzass4  10191  fzocatel  10335  zsupcllemstep  10379  zssinfcl  10382  suprzubdc  10386  zsupssdc  10388  suprzcl2dc  10389  exbtwnzlemex  10399  rebtwn2z  10404  qbtwnre  10406  modqid  10501  modqcyc  10511  modqaddabs  10514  modqaddmod  10515  mulqaddmodid  10516  modqadd2mod  10526  modqltm1p1mod  10528  modqsubmod  10534  modqsubmodmod  10535  modqmulmod  10541  modqmulmodr  10542  modqaddmulmod  10543  modqsubdir  10545  frec2uzisod  10559  iseqovex  10610  seqvalcd  10613  seq1g  10615  seqf  10616  seqovcd  10619  seqm1g  10626  seq3fveq2  10627  seq3shft2  10633  seqshft2g  10634  monoord  10637  seq3split  10640  seqsplitg  10641  iseqf1olemnab  10653  seqf1oglem1  10671  seqf1og  10673  seq3id2  10678  seqhomog  10682  seq3distr  10684  expcl2lemap  10703  expnegzap  10725  ltexp2a  10743  le2sq2  10767  nn0ltexp2  10861  nn0opth2  10876  bcval5  10915  hashcl  10933  hashen  10936  fihashdom  10955  hashunlem  10956  hashun  10957  fimaxq  10979  zfz1isolem1  10992  zfz1iso  10993  lencl  11005  sswrd  11010  fstwrdne0  11040  lswlgt0cl  11053  swrdval  11109  cvg1nlemres  11340  cvg1n  11341  recvguniq  11350  resqrexlemp1rp  11361  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemex  11380  sqrtmul  11390  sqrtsq  11399  absexpzap  11435  absle  11444  abs3lem  11466  amgm2  11473  maxleastlt  11570  maxltsup  11573  fimaxre2  11582  xrmaxleastlt  11611  xrmaxltsup  11613  xrmaxaddlem  11615  climcn2  11664  addcn2  11665  mulcn2  11667  reccn2ap  11668  climcau  11702  summodclem2  11737  summodc  11738  fsumf1o  11745  fisumss  11747  fsum3cvg3  11751  fsumcl2lem  11753  fsumadd  11761  fsum2dlemstep  11789  mptfzshft  11797  fsumrev  11798  fsummulc2  11803  modfsummod  11813  fsumrelem  11826  binom  11839  cvgratnn  11886  mertenslemub  11889  prodmodc  11933  zproddc  11934  fprodf1o  11943  fprodssdc  11945  fprodmul  11946  fprodrev  11974  fprod2dlemstep  11977  efcllem  12014  tanaddaplem  12093  dvdsval2  12145  moddvds  12154  dvdsabseq  12202  dvdsflip  12206  oexpneg  12232  fldivndvdslt  12292  bitsfi  12312  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemeu  12372  dfgcd3  12375  bezout  12376  dvdsmulgcd  12390  bezoutr  12397  nninfctlemfo  12405  ialgrlem1st  12408  lcmgcdlem  12443  coprmdvds2  12459  qredeu  12463  rpdvds  12465  isprm5lem  12507  isprm6  12513  pw2dvdslemn  12531  nonsq  12573  crth  12590  eulerthlemh  12597  pclemdc  12655  pcprendvds2  12658  pceu  12662  pcval  12663  pczpre  12664  pcmul  12668  pcqmul  12670  pcqcl  12673  pcid  12691  pcneg  12692  pcgcd1  12695  pc2dvds  12697  pcprmpw2  12700  difsqpwdvds  12705  pcmpt  12710  pockthg  12724  1arith  12734  mul4sq  12761  4sqexercise2  12766  ennnfonelemg  12818  ennnfonelemex  12829  ennnfonelemrnh  12831  ennnfonelemrn  12834  ennnfonelemdm  12835  ennnfonelemnn0  12837  ennnfonelemim  12839  ennnfone  12840  ctinfomlemom  12842  ctinf  12845  ctiunctlemfo  12854  nninfdclemcl  12863  nninfdclemf  12864  nninfdclemp1  12865  unbendc  12869  isstruct2r  12887  setscom  12916  qusval  13199  ercpbl  13207  opifismgmdc  13247  grpinvalem  13261  grprida  13263  igsumvalx  13265  gsumfzval  13267  gsumpropd2  13269  gsumval2  13273  sgrppropd  13289  prdssgrpd  13291  mndpropd  13316  issubmnd  13318  submnd0  13320  prdsmndd  13324  mhmf1o  13346  0mhm  13362  resmhm  13363  mhmco  13366  mhmima  13367  mhmeql  13368  gsumwsubmcl  13372  gsumfzcl  13375  grppropd  13393  grpinvid1  13428  grpinvid2  13429  grplcan  13438  grplmulf1o  13450  grpnpncan0  13472  dfgrp3mlem  13474  grplactcnv  13478  pwssub  13489  mulgval  13502  mulgfng  13504  mulg1  13509  mulgnnp1  13510  mulgneg  13520  mulgnndir  13531  mulgdirlem  13533  mulgnn0ass  13538  mulgass  13539  subgmulg  13568  issubg4m  13573  subgintm  13578  0nsg  13594  eqgcpbl  13608  ghmmulg  13636  ghmpreima  13646  ghmeql  13647  ghmnsgima  13648  ghmnsgpreima  13649  ghmf1  13653  ghmf1o  13655  conjghm  13656  conjnmzb  13660  qusghm  13662  ablpncan3  13697  invghm  13709  eqgabl  13710  qusecsub  13711  gsumfzreidx  13717  gsumfzsubmcl  13718  gsumfzmptfidmadd  13719  gsumfzmhm  13723  imasrng  13762  qusrng  13764  srglmhm  13799  srgrmhm  13800  ringpropd  13844  ringlghm  13867  ringrghm  13868  imasring  13870  qusring2  13872  opprrngbg  13884  dvdsrvald  13899  dvdsrd  13900  dvdsrex  13904  dvdsrtr  13907  unitgrp  13922  unitpropdg  13954  rhmopp  13982  isnzr2  13990  issubrng2  14016  subrngintm  14018  subrgintm  14049  rhmpropd  14060  aprap  14092  lmodprop2d  14154  rmodislmodlem  14156  lssvacl  14171  lssvsubcl  14172  lssvscl  14181  islss3  14185  lsspropdg  14237  rnglidlmcl  14286  2idlcpblrng  14329  crngridl  14336  expghmap  14413  mulgghm2  14414  mulgrhm  14415  znf1o  14457  znleval  14459  znidom  14463  psrval  14472  mplsubgfilemcl  14505  epttop  14606  topssnei  14678  restbasg  14684  restopnb  14697  cnfval  14710  cnpfval  14711  iscnp4  14734  cnpnei  14735  cnptopco  14738  cncnp  14746  cnrest2  14752  cnptoprest  14755  cnptoprest2  14756  lmss  14762  lmtopcnp  14766  neitx  14784  txcnp  14787  txrest  14792  txdis  14793  txlm  14795  cnmpt21  14807  imasnopn  14815  xmetres2  14895  blvalps  14904  blval  14905  bl2in  14919  blhalf  14924  blssps  14943  blss  14944  blssexps  14945  blssex  14946  ssblex  14947  blin2  14948  metss2lem  15013  bdmetval  15016  bdmopn  15020  metrest  15022  xmetxp  15023  xmetxpbl  15024  xmettx  15026  metcnp3  15027  txmetcnp  15034  addcncntoplem  15077  elcncf2  15090  mulc1cncf  15105  cncfco  15107  cncfmet  15108  mulcncf  15124  dedekindeulemub  15134  dedekindeulemloc  15135  dedekindeulemlu  15137  dedekindeu  15139  suplociccex  15141  dedekindicclemub  15143  dedekindicclemloc  15144  dedekindicclemlu  15146  dedekindicc  15149  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthdec  15160  ivthreinc  15161  dich0  15168  limcimolemlt  15180  limcimo  15181  cnplimccntop  15186  limccnp2lem  15192  limccnp2cntop  15193  dvfvalap  15197  dvmptfsum  15241  dveflem  15242  plyco  15275  plycn  15278  plyrecj  15279  reeff1olem  15287  reeff1oleme  15288  eflt  15291  sin0pilem2  15298  pilem3  15299  ptolemy  15340  ioocosf1o  15370  cxplt  15432  cxple  15433  cxplt3  15436  apcxp2  15455  rprelogbmul  15471  rprelogbdiv  15473  logbgt0b  15482  logbgcd1irrap  15486  fsumdvdsmul  15507  perfectlem2  15516  lgsdir2lem5  15553  lgsdir  15556  lgsdi  15558  lgsne0  15559  gausslemma2dlem1f1o  15581  lgseisenlem2  15592  lgsquadlem1  15598  lgsquadlem2  15599  lgsquad2lem2  15603  lgsquad2  15604  2sqlem6  15641  2sqlem10  15646  nnti  16003  pwtrufal  16008  pwf1oexmid  16010  sssneq  16013  qdencn  16040  cvgcmp2n  16046  trilpolemlt1  16054  trirec0  16057  trirec0xor  16058  redc0  16070  reap0  16071  cndcap  16072  nconstwlpolemgt0  16077  neap0mkv  16082  supfz  16084  inffz  16085