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  1064  simp2rl  1068  simp3rl  1072  rmob  3070  disjiun  4013  reg3exmidlemwe  4596  0xp  4724  imainss  5062  iotam  5227  fvmptt  5628  fcof1o  5811  isotr  5838  riota5f  5877  ovmpodf  6029  unielxp  6200  fnmpoovd  6241  1stconst  6247  2ndconst  6248  cnvf1olem  6250  tfrlemi14d  6359  tfrexlem  6360  tfr1onlemres  6375  tfrcllemres  6388  tfrcldm  6389  frecabcl  6425  nnaordi  6534  swoer  6588  qliftfun  6644  ecopovsymg  6661  th3qlem1  6664  pw2f1odclem  6863  mapen  6875  mapxpen  6877  fidifsnen  6899  fisbth  6912  findcard2d  6920  findcard2sd  6921  diffisn  6922  diffifi  6923  ac6sfi  6927  fimax2gtri  6930  fientri3  6944  nnwetri  6945  unsnfi  6948  unsnfidcex  6949  unsnfidcel  6950  fisseneq  6961  fidcenumlemrk  6984  fidcenumlemr  6985  isbth  6997  ordiso2  7065  difinfsnlem  7129  difinfinf  7131  ctmlemr  7138  ctssdccl  7141  fodjum  7175  fodju0  7176  omniwomnimkv  7196  exmidfodomrlemrALT  7233  netap  7284  exmidmotap  7291  cc1  7295  cc2lem  7296  cc3  7298  cc4f  7299  cc4n  7301  dfplpq2  7384  dfmpq2  7385  mulpipqqs  7403  distrnqg  7417  ltexnqq  7438  subhalfnqq  7444  distrnq0  7489  prarloclemup  7525  prarloclem3  7527  prarloc  7533  genplt2i  7540  nqprl  7581  nqpru  7582  prmuloc  7596  mullocpr  7601  distrlem4prl  7614  distrlem4pru  7615  ltaddpr  7627  ltexprlemopl  7631  ltexprlemlol  7632  ltexprlemopu  7633  ltexprlemupu  7634  ltexprlemrl  7640  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  ltaprlem  7648  ltaprg  7649  prplnqu  7650  addextpr  7651  recexprlemdisj  7660  recexprlemloc  7661  recexprlem1ssl  7663  aptiprleml  7669  aptiprlemu  7670  ltmprr  7672  archpr  7673  cauappcvgprlemopl  7676  cauappcvgprlemopu  7678  cauappcvgprlemdisj  7681  cauappcvgprlemloc  7682  cauappcvgprlem1  7689  cauappcvgprlem2  7690  cauappcvgprlemlim  7691  caucvgprlemnkj  7696  caucvgprlemopl  7699  caucvgprlemopu  7701  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlem2  7710  caucvgprprlemnkltj  7719  caucvgprprlemnkeqj  7720  caucvgprprlemnjltk  7721  caucvgprprlemmu  7725  caucvgprprlemopl  7727  caucvgprprlemopu  7729  caucvgprprlemdisj  7732  caucvgprprlemloc  7733  caucvgprprlemexbt  7736  caucvgprprlemaddq  7738  caucvgprprlem2  7740  suplocexprlemrl  7747  suplocexprlemmu  7748  suplocexprlemru  7749  suplocexprlemdisj  7750  suplocexprlemloc  7751  suplocexprlemex  7752  suplocexprlemub  7753  suplocexprlemlub  7754  recexgt0sr  7803  mulgt0sr  7808  prsrriota  7818  caucvgsrlemoffres  7830  suplocsrlem  7838  cnm  7862  addcnsr  7864  mulcnsr  7865  mulcnsrec  7873  axaddcl  7894  axmulcl  7896  axmulcom  7901  rereceu  7919  recriota  7920  axcaucvglemres  7929  axpre-suploclemres  7931  lelttr  8077  ltletr  8078  readdcan  8128  addcan  8168  addcan2  8169  addsub4  8231  ltadd2  8407  le2add  8432  lt2add  8433  lt2sub  8448  le2sub  8449  eqord1  8471  rimul  8573  rereim  8574  ltmul1  8580  apreim  8591  mulreim  8592  apcotr  8595  apadd1  8596  addext  8598  apneg  8599  mulext1  8600  mulext  8602  ltleap  8620  aprcl  8634  mulap0  8642  mulcanapd  8649  receuap  8657  recapb  8659  rec11ap  8698  rec11rap  8699  divdivdivap  8701  ddcanap  8714  divadddivap  8715  conjmulap  8717  subrecap  8827  prodgt0gt0  8839  prodge0  8842  ltmul12a  8848  lemulge11  8854  lt2mul2div  8867  ltrec  8871  lerec  8872  lt2msq  8874  lerec2  8877  le2msq  8889  msq11  8890  ledivp1  8891  mulle0r  8932  suprzclex  9382  peano5uzti  9392  supinfneg  9627  infsupneg  9628  qapne  9671  xrlelttr  9838  xrltletr  9839  xrre  9852  xaddge0  9910  xle2add  9911  xlt2add  9912  divelunit  10034  fzass4  10094  fzocatel  10231  exbtwnzlemex  10282  rebtwn2z  10287  qbtwnre  10289  modqid  10382  modqcyc  10392  modqaddabs  10395  modqaddmod  10396  mulqaddmodid  10397  modqadd2mod  10407  modqltm1p1mod  10409  modqsubmod  10415  modqsubmodmod  10416  modqmulmod  10422  modqmulmodr  10423  modqaddmulmod  10424  modqsubdir  10426  frec2uzisod  10440  iseqovex  10489  seqvalcd  10492  seqf  10494  seqovcd  10496  seq3fveq2  10502  seq3shft2  10506  monoord  10509  seq3split  10512  iseqf1olemnab  10521  seq3id2  10542  seq3distr  10547  expcl2lemap  10566  expnegzap  10588  ltexp2a  10606  le2sq2  10630  nn0ltexp2  10724  nn0opth2  10739  bcval5  10778  hashcl  10796  hashen  10799  fihashdom  10818  hashunlem  10819  hashun  10820  fimaxq  10842  zfz1isolem1  10855  zfz1iso  10856  cvg1nlemres  11029  cvg1n  11030  recvguniq  11039  resqrexlemp1rp  11050  resqrexlemoverl  11065  resqrexlemglsq  11066  resqrexlemex  11069  sqrtmul  11079  sqrtsq  11088  absexpzap  11124  absle  11133  abs3lem  11155  amgm2  11162  maxleastlt  11259  maxltsup  11262  fimaxre2  11270  xrmaxleastlt  11299  xrmaxltsup  11301  xrmaxaddlem  11303  climcn2  11352  addcn2  11353  mulcn2  11355  reccn2ap  11356  climcau  11390  summodclem2  11425  summodc  11426  fsumf1o  11433  fisumss  11435  fsum3cvg3  11439  fsumcl2lem  11441  fsumadd  11449  fsum2dlemstep  11477  mptfzshft  11485  fsumrev  11486  fsummulc2  11491  modfsummod  11501  fsumrelem  11514  binom  11527  cvgratnn  11574  mertenslemub  11577  prodmodc  11621  zproddc  11622  fprodf1o  11631  fprodssdc  11633  fprodmul  11634  fprodrev  11662  fprod2dlemstep  11665  efcllem  11702  tanaddaplem  11781  dvdsval2  11832  moddvds  11841  dvdsabseq  11888  dvdsflip  11892  oexpneg  11917  fldivndvdslt  11975  zsupcllemstep  11981  zssinfcl  11984  suprzubdc  11988  zsupssdc  11990  suprzcl2dc  11991  bezoutlemnewy  12032  bezoutlemstep  12033  bezoutlemeu  12043  dfgcd3  12046  bezout  12047  dvdsmulgcd  12061  bezoutr  12068  ialgrlem1st  12077  lcmgcdlem  12112  coprmdvds2  12128  qredeu  12132  rpdvds  12134  isprm5lem  12176  isprm6  12182  pw2dvdslemn  12200  nonsq  12242  crth  12259  eulerthlemh  12266  pclemdc  12323  pcprendvds2  12326  pceu  12330  pcval  12331  pczpre  12332  pcmul  12336  pcqmul  12338  pcqcl  12341  pcid  12359  pcneg  12360  pcgcd1  12363  pc2dvds  12365  pcprmpw2  12368  difsqpwdvds  12373  pcmpt  12378  pockthg  12392  1arith  12402  mul4sq  12429  4sqexercise2  12434  ennnfonelemg  12457  ennnfonelemex  12468  ennnfonelemrnh  12470  ennnfonelemrn  12473  ennnfonelemdm  12474  ennnfonelemnn0  12476  ennnfonelemim  12478  ennnfone  12479  ctinfomlemom  12481  ctinf  12484  ctiunctlemfo  12493  nninfdclemcl  12502  nninfdclemf  12503  nninfdclemp1  12504  unbendc  12508  isstruct2r  12526  setscom  12555  qusval  12803  ercpbl  12810  opifismgmdc  12850  grpinvalem  12864  grprida  12866  igsumvalx  12868  gsumpropd2  12871  gsumval2  12875  sgrppropd  12891  mndpropd  12916  issubmnd  12918  submnd0  12920  mhmf1o  12937  0mhm  12953  resmhm  12954  mhmco  12957  mhmima  12958  mhmeql  12959  grppropd  12977  grpinvid1  13011  grpinvid2  13012  grplcan  13021  grplmulf1o  13033  grpnpncan0  13055  dfgrp3mlem  13057  grplactcnv  13061  mulgval  13079  mulgfng  13081  mulg1  13086  mulgnnp1  13087  mulgneg  13097  mulgnndir  13108  mulgdirlem  13110  mulgnn0ass  13115  mulgass  13116  subgmulg  13144  issubg4m  13149  subgintm  13154  0nsg  13170  eqgcpbl  13184  ghmmulg  13212  ghmpreima  13222  ghmeql  13223  ghmnsgima  13224  ghmnsgpreima  13225  ghmf1  13229  ghmf1o  13231  conjghm  13232  conjnmzb  13236  qusghm  13238  ablpncan3  13273  eqgabl  13284  qusecsub  13285  imasrng  13327  qusrng  13329  srglmhm  13364  srgrmhm  13365  ringpropd  13409  imasring  13431  qusring2  13433  opprrngbg  13445  dvdsrvald  13460  dvdsrd  13461  dvdsrex  13465  dvdsrtr  13468  unitgrp  13483  unitpropdg  13515  rhmopp  13543  issubrng2  13574  subrngintm  13576  subrgintm  13607  aprap  13619  lmodprop2d  13681  rmodislmodlem  13683  lssvacl  13698  lssvsubcl  13699  lssvscl  13708  islss3  13712  lsspropdg  13764  rnglidlmcl  13813  2idlcpblrng  13855  crngridl  13861  mulgghm2  13923  mulgrhm  13924  psrval  13961  epttop  14067  topssnei  14139  restbasg  14145  restopnb  14158  cnfval  14171  cnpfval  14172  iscnp4  14195  cnpnei  14196  cnptopco  14199  cncnp  14207  cnrest2  14213  cnptoprest  14216  cnptoprest2  14217  lmss  14223  lmtopcnp  14227  neitx  14245  txcnp  14248  txrest  14253  txdis  14254  txlm  14256  cnmpt21  14268  imasnopn  14276  xmetres2  14356  blvalps  14365  blval  14366  bl2in  14380  blhalf  14385  blssps  14404  blss  14405  blssexps  14406  blssex  14407  ssblex  14408  blin2  14409  metss2lem  14474  bdmetval  14477  bdmopn  14481  metrest  14483  xmetxp  14484  xmetxpbl  14485  xmettx  14487  metcnp3  14488  txmetcnp  14495  addcncntoplem  14528  elcncf2  14538  mulc1cncf  14553  cncfco  14555  cncfmet  14556  mulcncf  14568  dedekindeulemub  14573  dedekindeulemloc  14574  dedekindeulemlu  14576  dedekindeu  14578  suplociccex  14580  dedekindicclemub  14582  dedekindicclemloc  14583  dedekindicclemlu  14585  dedekindicc  14588  ivthinclemlopn  14591  ivthinclemuopn  14593  ivthdec  14599  limcimolemlt  14610  limcimo  14611  cnplimccntop  14616  limccnp2lem  14622  limccnp2cntop  14623  dvfvalap  14627  dveflem  14664  reeff1olem  14669  reeff1oleme  14670  eflt  14673  sin0pilem2  14680  pilem3  14681  ptolemy  14722  ioocosf1o  14752  cxplt  14813  cxple  14814  cxplt3  14817  apcxp2  14835  rprelogbmul  14850  rprelogbdiv  14852  logbgt0b  14861  logbgcd1irrap  14865  lgsdir2lem5  14911  lgsdir  14914  lgsdi  14916  lgsne0  14917  lgseisenlem2  14929  2sqlem6  14945  2sqlem10  14950  nnti  15223  pwtrufal  15226  pwf1oexmid  15228  sssneq  15230  qdencn  15254  cvgcmp2n  15260  trilpolemlt1  15268  trirec0  15271  trirec0xor  15272  redc0  15284  reap0  15285  cndcap  15286  nconstwlpolemgt0  15291  neap0mkv  15296  supfz  15298  inffz  15299