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  1062  simp2rl  1066  simp3rl  1070  rmob  3053  disjiun  3993  reg3exmidlemwe  4572  0xp  4700  imainss  5036  iotam  5200  fvmptt  5599  fcof1o  5780  isotr  5807  riota5f  5845  ovmpodf  5996  unielxp  6165  fnmpoovd  6206  1stconst  6212  2ndconst  6213  cnvf1olem  6215  tfrlemi14d  6324  tfrexlem  6325  tfr1onlemres  6340  tfrcllemres  6353  tfrcldm  6354  frecabcl  6390  nnaordi  6499  swoer  6553  qliftfun  6607  ecopovsymg  6624  th3qlem1  6627  mapen  6836  mapxpen  6838  fidifsnen  6860  fisbth  6873  findcard2d  6881  findcard2sd  6882  diffisn  6883  diffifi  6884  ac6sfi  6888  fimax2gtri  6891  fientri3  6904  nnwetri  6905  unsnfi  6908  unsnfidcex  6909  unsnfidcel  6910  fisseneq  6921  fidcenumlemrk  6943  fidcenumlemr  6944  isbth  6956  ordiso2  7024  difinfsnlem  7088  difinfinf  7090  ctmlemr  7097  ctssdccl  7100  fodjum  7134  fodju0  7135  omniwomnimkv  7155  exmidfodomrlemrALT  7192  cc1  7239  cc2lem  7240  cc3  7242  cc4f  7243  cc4n  7245  dfplpq2  7328  dfmpq2  7329  mulpipqqs  7347  distrnqg  7361  ltexnqq  7382  subhalfnqq  7388  distrnq0  7433  prarloclemup  7469  prarloclem3  7471  prarloc  7477  genplt2i  7484  nqprl  7525  nqpru  7526  prmuloc  7540  mullocpr  7545  distrlem4prl  7558  distrlem4pru  7559  ltaddpr  7571  ltexprlemopl  7575  ltexprlemlol  7576  ltexprlemopu  7577  ltexprlemupu  7578  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  ltaprlem  7592  ltaprg  7593  prplnqu  7594  addextpr  7595  recexprlemdisj  7604  recexprlemloc  7605  recexprlem1ssl  7607  aptiprleml  7613  aptiprlemu  7614  ltmprr  7616  archpr  7617  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlem1  7633  cauappcvgprlem2  7634  cauappcvgprlemlim  7635  caucvgprlemnkj  7640  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlem2  7654  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnjltk  7665  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemdisj  7676  caucvgprprlemloc  7677  caucvgprprlemexbt  7680  caucvgprprlemaddq  7682  caucvgprprlem2  7684  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  suplocexprlemlub  7698  recexgt0sr  7747  mulgt0sr  7752  prsrriota  7762  caucvgsrlemoffres  7774  suplocsrlem  7782  cnm  7806  addcnsr  7808  mulcnsr  7809  mulcnsrec  7817  axaddcl  7838  axmulcl  7840  axmulcom  7845  rereceu  7863  recriota  7864  axcaucvglemres  7873  axpre-suploclemres  7875  lelttr  8020  ltletr  8021  readdcan  8071  addcan  8111  addcan2  8112  addsub4  8174  ltadd2  8350  le2add  8375  lt2add  8376  lt2sub  8391  le2sub  8392  eqord1  8414  rimul  8516  rereim  8517  ltmul1  8523  apreim  8534  mulreim  8535  apcotr  8538  apadd1  8539  addext  8541  apneg  8542  mulext1  8543  mulext  8545  ltleap  8563  aprcl  8577  mulap0  8584  mulcanapd  8591  receuap  8599  recapb  8601  rec11ap  8640  rec11rap  8641  divdivdivap  8643  ddcanap  8656  divadddivap  8657  conjmulap  8659  subrecap  8769  prodgt0gt0  8781  prodge0  8784  ltmul12a  8790  lemulge11  8796  lt2mul2div  8809  ltrec  8813  lerec  8814  lt2msq  8816  lerec2  8819  le2msq  8831  msq11  8832  ledivp1  8833  mulle0r  8874  suprzclex  9324  peano5uzti  9334  supinfneg  9568  infsupneg  9569  qapne  9612  xrlelttr  9777  xrltletr  9778  xrre  9791  xaddge0  9849  xle2add  9850  xlt2add  9851  divelunit  9973  fzass4  10032  fzocatel  10169  exbtwnzlemex  10220  rebtwn2z  10225  qbtwnre  10227  modqid  10319  modqcyc  10329  modqaddabs  10332  modqaddmod  10333  mulqaddmodid  10334  modqadd2mod  10344  modqltm1p1mod  10346  modqsubmod  10352  modqsubmodmod  10353  modqmulmod  10359  modqmulmodr  10360  modqaddmulmod  10361  modqsubdir  10363  frec2uzisod  10377  iseqovex  10426  seqvalcd  10429  seqf  10431  seqovcd  10433  seq3fveq2  10439  seq3shft2  10443  monoord  10446  seq3split  10449  iseqf1olemnab  10458  seq3id2  10479  seq3distr  10483  expcl2lemap  10502  expnegzap  10524  ltexp2a  10542  le2sq2  10565  nn0ltexp2  10658  nn0opth2  10672  bcval5  10711  hashcl  10729  hashen  10732  fihashdom  10751  hashunlem  10752  hashun  10753  fimaxq  10775  zfz1isolem1  10788  zfz1iso  10789  cvg1nlemres  10962  cvg1n  10963  recvguniq  10972  resqrexlemp1rp  10983  resqrexlemoverl  10998  resqrexlemglsq  10999  resqrexlemex  11002  sqrtmul  11012  sqrtsq  11021  absexpzap  11057  absle  11066  abs3lem  11088  amgm2  11095  maxleastlt  11192  maxltsup  11195  fimaxre2  11203  xrmaxleastlt  11232  xrmaxltsup  11234  xrmaxaddlem  11236  climcn2  11285  addcn2  11286  mulcn2  11288  reccn2ap  11289  climcau  11323  summodclem2  11358  summodc  11359  fsumf1o  11366  fisumss  11368  fsum3cvg3  11372  fsumcl2lem  11374  fsumadd  11382  fsum2dlemstep  11410  mptfzshft  11418  fsumrev  11419  fsummulc2  11424  modfsummod  11434  fsumrelem  11447  binom  11460  cvgratnn  11507  mertenslemub  11510  prodmodc  11554  zproddc  11555  fprodf1o  11564  fprodssdc  11566  fprodmul  11567  fprodrev  11595  fprod2dlemstep  11598  efcllem  11635  tanaddaplem  11714  dvdsval2  11765  moddvds  11774  dvdsabseq  11820  dvdsflip  11824  oexpneg  11849  fldivndvdslt  11907  zsupcllemstep  11913  zssinfcl  11916  suprzubdc  11920  zsupssdc  11922  suprzcl2dc  11923  bezoutlemnewy  11964  bezoutlemstep  11965  bezoutlemeu  11975  dfgcd3  11978  bezout  11979  dvdsmulgcd  11993  bezoutr  12000  ialgrlem1st  12009  lcmgcdlem  12044  coprmdvds2  12060  qredeu  12064  rpdvds  12066  isprm5lem  12108  isprm6  12114  pw2dvdslemn  12132  nonsq  12174  crth  12191  eulerthlemh  12198  pclemdc  12255  pcprendvds2  12258  pceu  12262  pcval  12263  pczpre  12264  pcmul  12268  pcqmul  12270  pcqcl  12273  pcid  12290  pcneg  12291  pcgcd1  12294  pc2dvds  12296  pcprmpw2  12299  difsqpwdvds  12304  pcmpt  12308  pockthg  12322  1arith  12332  mul4sq  12359  ennnfonelemg  12371  ennnfonelemex  12382  ennnfonelemrnh  12384  ennnfonelemrn  12387  ennnfonelemdm  12388  ennnfonelemnn0  12390  ennnfonelemim  12392  ennnfone  12393  ctinfomlemom  12395  ctinf  12398  ctiunctlemfo  12407  nninfdclemcl  12416  nninfdclemf  12417  nninfdclemp1  12418  unbendc  12422  isstruct2r  12440  setscom  12469  opifismgmdc  12665  grprinvlem  12679  grpridd  12681  mndpropd  12716  mhmf1o  12733  0mhm  12744  mhmco  12745  mhmima  12746  mhmeql  12747  grppropd  12764  grpinvid1  12795  grpinvid2  12796  grplcan  12802  grplmulf1o  12814  grpnpncan0  12836  dfgrp3mlem  12838  grplactcnv  12842  mulgval  12856  mulgfng  12857  mulg1  12860  mulgnnp1  12861  mulgneg  12871  mulgnndir  12881  mulgdirlem  12883  mulgnn0ass  12888  mulgass  12889  ablpncan3  12928  srglmhm  12982  srgrmhm  12983  ringpropd  13022  epttop  13170  topssnei  13242  restbasg  13248  restopnb  13261  cnfval  13274  cnpfval  13275  iscnp4  13298  cnpnei  13299  cnptopco  13302  cncnp  13310  cnrest2  13316  cnptoprest  13319  cnptoprest2  13320  lmss  13326  lmtopcnp  13330  neitx  13348  txcnp  13351  txrest  13356  txdis  13357  txlm  13359  cnmpt21  13371  imasnopn  13379  xmetres2  13459  blvalps  13468  blval  13469  bl2in  13483  blhalf  13488  blssps  13507  blss  13508  blssexps  13509  blssex  13510  ssblex  13511  blin2  13512  metss2lem  13577  bdmetval  13580  bdmopn  13584  metrest  13586  xmetxp  13587  xmetxpbl  13588  xmettx  13590  metcnp3  13591  txmetcnp  13598  addcncntoplem  13631  elcncf2  13641  mulc1cncf  13656  cncfco  13658  cncfmet  13659  mulcncf  13671  dedekindeulemub  13676  dedekindeulemloc  13677  dedekindeulemlu  13679  dedekindeu  13681  suplociccex  13683  dedekindicclemub  13685  dedekindicclemloc  13686  dedekindicclemlu  13688  dedekindicc  13691  ivthinclemlopn  13694  ivthinclemuopn  13696  ivthdec  13702  limcimolemlt  13713  limcimo  13714  cnplimccntop  13719  limccnp2lem  13725  limccnp2cntop  13726  dvfvalap  13730  dveflem  13767  reeff1olem  13772  reeff1oleme  13773  eflt  13776  sin0pilem2  13783  pilem3  13784  ptolemy  13825  ioocosf1o  13855  cxplt  13916  cxple  13917  cxplt3  13920  apcxp2  13938  rprelogbmul  13953  rprelogbdiv  13955  logbgt0b  13964  logbgcd1irrap  13968  lgsdir2lem5  14013  lgsdir  14016  lgsdi  14018  lgsne0  14019  2sqlem6  14036  2sqlem10  14041  nnti  14313  pwtrufal  14316  pwf1oexmid  14318  sssneq  14321  qdencn  14345  cvgcmp2n  14351  trilpolemlt1  14359  trirec0  14362  trirec0xor  14363  redc0  14375  reap0  14376  nconstwlpolemgt0  14381  supfz  14386  inffz  14387