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  3082  disjiun  4029  reg3exmidlemwe  4616  0xp  4744  imainss  5086  iotam  5251  fvmptt  5656  fcof1o  5839  isotr  5866  riota5f  5905  ovmpodf  6058  unielxp  6241  fnmpoovd  6282  1stconst  6288  2ndconst  6289  cnvf1olem  6291  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemres  6416  tfrcllemres  6429  tfrcldm  6430  frecabcl  6466  nnaordi  6575  swoer  6629  qliftfun  6685  ecopovsymg  6702  th3qlem1  6705  pw2f1odclem  6904  mapen  6916  mapxpen  6918  fidifsnen  6940  fisbth  6953  findcard2d  6961  findcard2sd  6962  diffisn  6963  diffifi  6964  ac6sfi  6968  fimax2gtri  6971  fientri3  6985  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  fidcenumlemrk  7029  fidcenumlemr  7030  isbth  7042  ordiso2  7110  difinfsnlem  7174  difinfinf  7176  ctmlemr  7183  ctssdccl  7186  fodjum  7221  fodju0  7222  omniwomnimkv  7242  exmidfodomrlemrALT  7284  netap  7339  exmidmotap  7346  cc1  7350  cc2lem  7351  cc3  7353  cc4f  7354  cc4n  7356  dfplpq2  7440  dfmpq2  7441  mulpipqqs  7459  distrnqg  7473  ltexnqq  7494  subhalfnqq  7500  distrnq0  7545  prarloclemup  7581  prarloclem3  7583  prarloc  7589  genplt2i  7596  nqprl  7637  nqpru  7638  prmuloc  7652  mullocpr  7657  distrlem4prl  7670  distrlem4pru  7671  ltaddpr  7683  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  ltaprlem  7704  ltaprg  7705  prplnqu  7706  addextpr  7707  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssl  7719  aptiprleml  7725  aptiprlemu  7726  ltmprr  7728  archpr  7729  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgprlemlim  7747  caucvgprlemnkj  7752  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlem2  7766  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemdisj  7788  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlem2  7796  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  suplocexprlemlub  7810  recexgt0sr  7859  mulgt0sr  7864  prsrriota  7874  caucvgsrlemoffres  7886  suplocsrlem  7894  cnm  7918  addcnsr  7920  mulcnsr  7921  mulcnsrec  7929  axaddcl  7950  axmulcl  7952  axmulcom  7957  rereceu  7975  recriota  7976  axcaucvglemres  7985  axpre-suploclemres  7987  lelttr  8134  ltletr  8135  readdcan  8185  addcan  8225  addcan2  8226  addsub4  8288  ltadd2  8465  le2add  8490  lt2add  8491  lt2sub  8506  le2sub  8507  eqord1  8529  rimul  8631  rereim  8632  ltmul1  8638  apreim  8649  mulreim  8650  apcotr  8653  apadd1  8654  addext  8656  apneg  8657  mulext1  8658  mulext  8660  ltleap  8678  aprcl  8692  mulap0  8700  mulcanapd  8707  receuap  8715  recapb  8717  rec11ap  8756  rec11rap  8757  divdivdivap  8759  ddcanap  8772  divadddivap  8773  conjmulap  8775  subrecap  8885  prodgt0gt0  8897  prodge0  8900  ltmul12a  8906  lemulge11  8912  lt2mul2div  8925  ltrec  8929  lerec  8930  lt2msq  8932  lerec2  8935  le2msq  8947  msq11  8948  ledivp1  8949  mulle0r  8990  suprzclex  9443  peano5uzti  9453  supinfneg  9688  infsupneg  9689  qapne  9732  xrlelttr  9900  xrltletr  9901  xrre  9914  xaddge0  9972  xle2add  9973  xlt2add  9974  divelunit  10096  fzass4  10156  fzocatel  10294  zsupcllemstep  10338  zssinfcl  10341  suprzubdc  10345  zsupssdc  10347  suprzcl2dc  10348  exbtwnzlemex  10358  rebtwn2z  10363  qbtwnre  10365  modqid  10460  modqcyc  10470  modqaddabs  10473  modqaddmod  10474  mulqaddmodid  10475  modqadd2mod  10485  modqltm1p1mod  10487  modqsubmod  10493  modqsubmodmod  10494  modqmulmod  10500  modqmulmodr  10501  modqaddmulmod  10502  modqsubdir  10504  frec2uzisod  10518  iseqovex  10569  seqvalcd  10572  seq1g  10574  seqf  10575  seqovcd  10578  seqm1g  10585  seq3fveq2  10586  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  iseqf1olemnab  10612  seqf1oglem1  10630  seqf1og  10632  seq3id2  10637  seqhomog  10641  seq3distr  10643  expcl2lemap  10662  expnegzap  10684  ltexp2a  10702  le2sq2  10726  nn0ltexp2  10820  nn0opth2  10835  bcval5  10874  hashcl  10892  hashen  10895  fihashdom  10914  hashunlem  10915  hashun  10916  fimaxq  10938  zfz1isolem1  10951  zfz1iso  10952  lencl  10958  sswrd  10963  fstwrdne0  10993  cvg1nlemres  11169  cvg1n  11170  recvguniq  11179  resqrexlemp1rp  11190  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemex  11209  sqrtmul  11219  sqrtsq  11228  absexpzap  11264  absle  11273  abs3lem  11295  amgm2  11302  maxleastlt  11399  maxltsup  11402  fimaxre2  11411  xrmaxleastlt  11440  xrmaxltsup  11442  xrmaxaddlem  11444  climcn2  11493  addcn2  11494  mulcn2  11496  reccn2ap  11497  climcau  11531  summodclem2  11566  summodc  11567  fsumf1o  11574  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fsum2dlemstep  11618  mptfzshft  11626  fsumrev  11627  fsummulc2  11632  modfsummod  11642  fsumrelem  11655  binom  11668  cvgratnn  11715  mertenslemub  11718  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  fprodrev  11803  fprod2dlemstep  11806  efcllem  11843  tanaddaplem  11922  dvdsval2  11974  moddvds  11983  dvdsabseq  12031  dvdsflip  12035  oexpneg  12061  fldivndvdslt  12121  bitsfi  12141  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemeu  12201  dfgcd3  12204  bezout  12205  dvdsmulgcd  12219  bezoutr  12226  nninfctlemfo  12234  ialgrlem1st  12237  lcmgcdlem  12272  coprmdvds2  12288  qredeu  12292  rpdvds  12294  isprm5lem  12336  isprm6  12342  pw2dvdslemn  12360  nonsq  12402  crth  12419  eulerthlemh  12426  pclemdc  12484  pcprendvds2  12487  pceu  12491  pcval  12492  pczpre  12493  pcmul  12497  pcqmul  12499  pcqcl  12502  pcid  12520  pcneg  12521  pcgcd1  12524  pc2dvds  12526  pcprmpw2  12529  difsqpwdvds  12534  pcmpt  12539  pockthg  12553  1arith  12563  mul4sq  12590  4sqexercise2  12595  ennnfonelemg  12647  ennnfonelemex  12658  ennnfonelemrnh  12660  ennnfonelemrn  12663  ennnfonelemdm  12664  ennnfonelemnn0  12666  ennnfonelemim  12668  ennnfone  12669  ctinfomlemom  12671  ctinf  12674  ctiunctlemfo  12683  nninfdclemcl  12692  nninfdclemf  12693  nninfdclemp1  12694  unbendc  12698  isstruct2r  12716  setscom  12745  qusval  13027  ercpbl  13035  opifismgmdc  13075  grpinvalem  13089  grprida  13091  igsumvalx  13093  gsumfzval  13095  gsumpropd2  13097  gsumval2  13101  sgrppropd  13117  prdssgrpd  13119  mndpropd  13144  issubmnd  13146  submnd0  13148  prdsmndd  13152  mhmf1o  13174  0mhm  13190  resmhm  13191  mhmco  13194  mhmima  13195  mhmeql  13196  gsumwsubmcl  13200  gsumfzcl  13203  grppropd  13221  grpinvid1  13256  grpinvid2  13257  grplcan  13266  grplmulf1o  13278  grpnpncan0  13300  dfgrp3mlem  13302  grplactcnv  13306  pwssub  13317  mulgval  13330  mulgfng  13332  mulg1  13337  mulgnnp1  13338  mulgneg  13348  mulgnndir  13359  mulgdirlem  13361  mulgnn0ass  13366  mulgass  13367  subgmulg  13396  issubg4m  13401  subgintm  13406  0nsg  13422  eqgcpbl  13436  ghmmulg  13464  ghmpreima  13474  ghmeql  13475  ghmnsgima  13476  ghmnsgpreima  13477  ghmf1  13481  ghmf1o  13483  conjghm  13484  conjnmzb  13488  qusghm  13490  ablpncan3  13525  invghm  13537  eqgabl  13538  qusecsub  13539  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  imasrng  13590  qusrng  13592  srglmhm  13627  srgrmhm  13628  ringpropd  13672  ringlghm  13695  ringrghm  13696  imasring  13698  qusring2  13700  opprrngbg  13712  dvdsrvald  13727  dvdsrd  13728  dvdsrex  13732  dvdsrtr  13735  unitgrp  13750  unitpropdg  13782  rhmopp  13810  isnzr2  13818  issubrng2  13844  subrngintm  13846  subrgintm  13877  rhmpropd  13888  aprap  13920  lmodprop2d  13982  rmodislmodlem  13984  lssvacl  13999  lssvsubcl  14000  lssvscl  14009  islss3  14013  lsspropdg  14065  rnglidlmcl  14114  2idlcpblrng  14157  crngridl  14164  expghmap  14241  mulgghm2  14242  mulgrhm  14243  znf1o  14285  znleval  14287  znidom  14291  psrval  14298  epttop  14412  topssnei  14484  restbasg  14490  restopnb  14503  cnfval  14516  cnpfval  14517  iscnp4  14540  cnpnei  14541  cnptopco  14544  cncnp  14552  cnrest2  14558  cnptoprest  14561  cnptoprest2  14562  lmss  14568  lmtopcnp  14572  neitx  14590  txcnp  14593  txrest  14598  txdis  14599  txlm  14601  cnmpt21  14613  imasnopn  14621  xmetres2  14701  blvalps  14710  blval  14711  bl2in  14725  blhalf  14730  blssps  14749  blss  14750  blssexps  14751  blssex  14752  ssblex  14753  blin2  14754  metss2lem  14819  bdmetval  14822  bdmopn  14826  metrest  14828  xmetxp  14829  xmetxpbl  14830  xmettx  14832  metcnp3  14833  txmetcnp  14840  addcncntoplem  14883  elcncf2  14896  mulc1cncf  14911  cncfco  14913  cncfmet  14914  mulcncf  14930  dedekindeulemub  14940  dedekindeulemloc  14941  dedekindeulemlu  14943  dedekindeu  14945  suplociccex  14947  dedekindicclemub  14949  dedekindicclemloc  14950  dedekindicclemlu  14952  dedekindicc  14955  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthdec  14966  ivthreinc  14967  dich0  14974  limcimolemlt  14986  limcimo  14987  cnplimccntop  14992  limccnp2lem  14998  limccnp2cntop  14999  dvfvalap  15003  dvmptfsum  15047  dveflem  15048  plyco  15081  plycn  15084  plyrecj  15085  reeff1olem  15093  reeff1oleme  15094  eflt  15097  sin0pilem2  15104  pilem3  15105  ptolemy  15146  ioocosf1o  15176  cxplt  15238  cxple  15239  cxplt3  15242  apcxp2  15261  rprelogbmul  15277  rprelogbdiv  15279  logbgt0b  15288  logbgcd1irrap  15292  fsumdvdsmul  15313  perfectlem2  15322  lgsdir2lem5  15359  lgsdir  15362  lgsdi  15364  lgsne0  15365  gausslemma2dlem1f1o  15387  lgseisenlem2  15398  lgsquadlem1  15404  lgsquadlem2  15405  lgsquad2lem2  15409  lgsquad2  15410  2sqlem6  15447  2sqlem10  15452  nnti  15725  pwtrufal  15730  pwf1oexmid  15732  sssneq  15735  qdencn  15762  cvgcmp2n  15768  trilpolemlt1  15776  trirec0  15779  trirec0xor  15780  redc0  15792  reap0  15793  cndcap  15794  nconstwlpolemgt0  15799  neap0mkv  15804  supfz  15806  inffz  15807