Theorem simprl 531

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  990  simp1rl  1089  simp2rl  1093  simp3rl  1097  rmob  3139  elpr2elpr  3885  disjiun  4109  reg3exmidlemwe  4706  opabssxpd  4791  0xp  4835  imainss  5183  iotam  5349  fvmptt  5774  fcof1o  5968  isotr  5995  riota5f  6038  ovmpodf  6193  unielxp  6381  fnmpoovd  6424  1stconst  6430  2ndconst  6431  cnvf1olem  6433  fvn0elsupp  6464  suppcofn  6479  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemres  6593  tfrcllemres  6606  tfrcldm  6607  frecabcl  6643  nnaordi  6754  swoer  6808  qliftfun  6864  ecopovsymg  6881  th3qlem1  6884  pw2f1odclem  7100  mapen  7112  mapxpen  7114  fidifsnen  7138  fisbth  7153  findcard2d  7161  findcard2sd  7162  diffisn  7163  diffifi  7164  ac6sfi  7168  fidcen  7169  fimax2gtri  7172  fientri3  7188  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fisseneq  7208  exmidssfi  7212  fidcenumlemrk  7237  fidcenumlemr  7238  isbth  7250  ordiso2  7339  difinfsnlem  7403  difinfinf  7405  ctmlemr  7412  ctssdccl  7415  fodjum  7450  fodju0  7451  omniwomnimkv  7471  exmidfodomrlemrALT  7519  netap  7584  exmidmotap  7591  cc1  7595  cc2lem  7596  cc3  7598  cc4f  7599  cc4n  7601  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  ltexnqq  7739  subhalfnqq  7745  distrnq0  7790  prarloclemup  7826  prarloclem3  7828  prarloc  7834  genplt2i  7841  nqprl  7882  nqpru  7883  prmuloc  7897  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltaddpr  7928  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprlem  7949  ltaprg  7950  prplnqu  7951  addextpr  7952  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssl  7964  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  archpr  7974  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlem2  8011  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  recexgt0sr  8104  mulgt0sr  8109  prsrriota  8119  caucvgsrlemoffres  8131  suplocsrlem  8139  cnm  8163  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axaddcl  8195  axmulcl  8197  axmulcom  8202  rereceu  8220  recriota  8221  axcaucvglemres  8230  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  readdcan  8430  addcan  8470  addcan2  8471  addsub4  8533  ltadd2  8711  le2add  8736  lt2add  8737  lt2sub  8752  le2sub  8753  eqord1  8775  rimul  8877  rereim  8878  ltmul1  8884  apreim  8895  mulreim  8896  apcotr  8899  apadd1  8900  addext  8902  apneg  8903  mulext1  8904  mulext  8906  ltleap  8924  aprcl  8938  mulap0  8946  mulcanapd  8953  receuap  8963  recapb  8965  rec11ap  9004  rec11rap  9005  divdivdivap  9007  ddcanap  9020  divadddivap  9021  conjmulap  9023  subrecap  9133  prodgt0gt0  9145  prodge0  9148  ltmul12a  9154  lemulge11  9160  lt2mul2div  9173  ltrec  9177  lerec  9178  lt2msq  9180  lerec2  9183  le2msq  9195  msq11  9196  ledivp1  9197  mulle0r  9238  suprzclex  9697  peano5uzti  9707  supinfneg  9948  infsupneg  9949  qapne  9992  xrlelttr  10161  xrltletr  10162  xrre  10175  xaddge0  10233  xle2add  10234  xlt2add  10235  divelunit  10357  fzass4  10420  fzocatel  10569  zsupcllemstep  10614  zssinfcl  10617  infssfzcldc  10621  infssfzledc  10622  suprzubdc  10623  zsupssdc  10625  suprzcl2dc  10626  exbtwnzlemex  10636  rebtwn2z  10641  qbtwnre  10643  modqid  10738  modqcyc  10748  modqaddabs  10751  modqaddmod  10752  mulqaddmodid  10753  modqadd2mod  10763  modqltm1p1mod  10765  modqsubmod  10771  modqsubmodmod  10772  modqmulmod  10778  modqmulmodr  10779  modqaddmulmod  10780  modqsubdir  10782  frec2uzisod  10796  iseqovex  10847  seqvalcd  10850  seq1g  10852  seqf  10853  seqovcd  10856  seqm1g  10863  seq3fveq2  10864  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  iseqf1olemnab  10890  seqf1oglem1  10908  seqf1og  10910  seq3id2  10915  seqhomog  10919  seq3distr  10921  expcl2lemap  10940  expnegzap  10962  ltexp2a  10980  le2sq2  11004  nn0ltexp2  11099  nn0opth2  11114  bcval5  11153  hashcl  11172  hashen  11175  fihashdom  11195  hashunlem  11196  hashun  11197  hashmap  11220  fimaxq  11222  hashfibclem  11234  hashfibc  11235  zfz1isolem1  11240  zfz1iso  11241  lencl  11256  sswrd  11261  fstwrdne0  11292  lswlgt0cl  11305  ccatw2s1p1g  11361  ccat2s1fstg  11364  swrdval  11368  wrdind  11442  wrd2ind  11443  swrdccatfn  11444  swrdccatin1  11445  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12  11453  pfxccat3a  11458  reuccatpfxs1  11467  cvg1nlemres  11698  cvg1n  11699  recvguniq  11708  resqrexlemp1rp  11719  resqrexlemoverl  11734  resqrexlemglsq  11735  resqrexlemex  11738  sqrtmul  11748  sqrtsq  11757  absexpzap  11793  absle  11802  abs3lem  11824  amgm2  11831  maxleastlt  11928  maxltsup  11931  fimaxre2  11940  xrmaxleastlt  11969  xrmaxltsup  11971  xrmaxaddlem  11973  climcn2  12022  addcn2  12023  mulcn2  12025  reccn2ap  12026  climcau  12060  summodclem2  12096  summodc  12097  fsumf1o  12104  fisumss  12106  fsum3cvg3  12110  fsumcl2lem  12112  fsumadd  12120  fsum2dlemstep  12148  mptfzshft  12156  fsumrev  12157  fsummulc2  12162  modfsummod  12172  fsumrelem  12185  binom  12198  cvgratnn  12245  mertenslemub  12248  prodmodc  12292  zproddc  12293  fprodf1o  12302  fprodssdc  12304  fprodmul  12305  fprodrev  12333  fprod2dlemstep  12336  efcllem  12373  tanaddaplem  12452  dvdsval2  12504  moddvds  12513  dvdsabseq  12561  dvdsflip  12565  oexpneg  12591  fldivndvdslt  12651  bitsfi  12671  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemeu  12731  dfgcd3  12734  bezout  12735  dvdsmulgcd  12749  bezoutr  12756  nninfctlemfo  12764  ialgrlem1st  12767  lcmgcdlem  12802  coprmdvds2  12818  qredeu  12822  rpdvds  12824  isprm5lem  12866  isprm6  12872  pw2dvdslemn  12890  nonsq  12932  crth  12949  eulerthlemh  12956  pclemdc  13014  pcprendvds2  13017  pceu  13021  pcval  13022  pczpre  13023  pcmul  13027  pcqmul  13029  pcqcl  13032  pcid  13050  pcneg  13051  pcgcd1  13054  pc2dvds  13056  pcprmpw2  13059  difsqpwdvds  13064  pcmpt  13069  pockthg  13083  1arith  13093  mul4sq  13120  4sqexercise2  13125  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemg  13241  ennnfonelemex  13252  ennnfonelemrnh  13254  ennnfonelemrn  13257  ennnfonelemdm  13258  ennnfonelemnn0  13260  ennnfonelemim  13262  ennnfone  13263  ctinfomlemom  13265  ctinf  13268  ctiunctlemfo  13277  nninfdclemcl  13286  nninfdclemf  13287  nninfdclemp1  13288  unbendc  13292  isstruct2r  13310  setscom  13339  qusval  13590  ercpbl  13598  opifismgmdc  13637  grpinvalem  13651  grprida  13653  igsumvalx  13655  gsumfzval  13657  gsumpropd2  13659  gsumval2  13663  sgrppropd  13679  mndpropd  13704  issubmnd  13706  submnd0  13708  mhmf1o  13728  0mhm  13744  resmhm  13745  mhmco  13748  mhmima  13749  mhmeql  13750  gsumwsubmcl  13754  gsumfzcl  13757  grppropd  13775  grpinvid1  13810  grpinvid2  13811  grplcan  13820  grplmulf1o  13832  grpnpncan0  13854  dfgrp3mlem  13856  grplactcnv  13860  mulgval  13878  mulgfng  13880  mulg1  13885  mulgnnp1  13886  mulgneg  13896  mulgnndir  13907  mulgdirlem  13909  mulgnn0ass  13914  mulgass  13915  subgmulg  13944  issubg4m  13949  subgintm  13954  0nsg  13970  eqgcpbl  13984  ghmmulg  14012  ghmpreima  14022  ghmeql  14023  ghmnsgima  14024  ghmnsgpreima  14025  ghmf1  14029  ghmf1o  14031  conjghm  14032  conjnmzb  14036  qusghm  14038  ablpncan3  14073  invghm  14085  eqgabl  14086  qusecsub  14087  gsumfzreidx  14093  gsumfzsubmcl  14094  gsumfzmptfidmadd  14095  gsumfzmhm  14099  gfsumval  14105  gfsumcl  14113  prdssgrpd  14136  prdsmndd  14139  pwssub  14161  imasrng  14198  qusrng  14200  srglmhm  14239  srgrmhm  14240  ringpropd  14284  ringlghm  14307  ringrghm  14308  imasring  14310  qusring2  14312  opprrngbg  14324  dvdsrvald  14341  dvdsrd  14342  dvdsrex  14346  dvdsrtr  14349  unitgrp  14364  unitpropdg  14396  rhmopp  14424  isnzr2  14432  issubrng2  14459  subrngintm  14461  subrgintm  14492  rhmpropd  14503  ringunitap  14534  aprap  14539  drngunitap  14549  lmodprop2d  14625  rmodislmodlem  14627  lssvacl  14642  lssvsubcl  14643  lssvscl  14652  islss3  14656  lsspropdg  14708  rnglidlmcl  14757  2idlcpblrng  14800  crngridl  14807  expghmap  14884  mulgghm2  14885  mulgrhm  14886  znf1o  14928  znleval  14930  znidom  14934  psrval  14943  psrbagcon  14955  psrbagconf1o  14957  mplsubgfilemcl  14983  epttop  15084  topssnei  15156  restbasg  15162  restopnb  15175  cnfval  15188  cnpfval  15189  iscnp4  15212  cnpnei  15213  cnptopco  15216  cncnp  15224  cnrest2  15230  cnptoprest  15233  cnptoprest2  15234  lmss  15240  lmtopcnp  15244  neitx  15262  txcnp  15265  txrest  15270  txdis  15271  txlm  15273  cnmpt21  15285  imasnopn  15293  xmetres2  15373  blvalps  15382  blval  15383  bl2in  15397  blhalf  15402  blssps  15421  blss  15422  blssexps  15423  blssex  15424  ssblex  15425  blin2  15426  metss2lem  15491  bdmetval  15494  bdmopn  15498  metrest  15500  xmetxp  15501  xmetxpbl  15502  xmettx  15504  metcnp3  15505  txmetcnp  15512  addcncntoplem  15555  elcncf2  15568  mulc1cncf  15583  cncfco  15585  cncfmet  15586  mulcncf  15602  dedekindeulemub  15612  dedekindeulemloc  15613  dedekindeulemlu  15615  dedekindeu  15617  suplociccex  15619  dedekindicclemub  15621  dedekindicclemloc  15622  dedekindicclemlu  15624  dedekindicc  15627  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthdec  15638  ivthreinc  15639  dich0  15646  limcimolemlt  15658  limcimo  15659  cnplimccntop  15664  limccnp2lem  15670  limccnp2cntop  15671  dvfvalap  15675  dvmptfsum  15719  dveflem  15720  plyco  15753  plycn  15756  plyrecj  15757  reeff1olem  15765  reeff1oleme  15766  eflt  15769  sin0pilem2  15776  pilem3  15777  ptolemy  15818  ioocosf1o  15848  cxplt  15910  cxple  15911  cxplt3  15914  apcxp2  15933  rprelogbmul  15949  rprelogbdiv  15951  logbgt0b  15960  logbgcd1irrap  15964  pellexlem3  15976  fsumdvdsmul  15988  perfectlem2  15997  lgsdir2lem5  16034  lgsdir  16037  lgsdi  16039  lgsne0  16040  gausslemma2dlem1f1o  16062  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2lem2  16084  lgsquad2  16085  2sqlem6  16122  2sqlem10  16127  upgredg  16268  uhgrissubgr  16385  subgrprop3  16386  upgrspanop  16407  umgrspanop  16408  usgrspanop  16409  vtxedgfi  16413  vtxlpfi  16414  upgr2wlkdc  16501  clwwlkccatlem  16524  eupth2lemsfi  16602  depindlem3  16632  nnti  16905  pwtrufal  16910  pwf1oexmid  16912  sssneq  16915  qdencn  16946  cvgcmp2n  16956  trilpolemlt1  16964  trirec0  16967  trirec0xor  16968  qdiff  16972  redc0  16981  reap0  16982  cndcap  16983  trimul0or  16984  nconstwlpolemgt0  16989  neap0mkv  16994  supfz  16996  inffz  16997