Theorem simprl 535

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 494	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dfifp2dc  994  simp1rl  1093  simp2rl  1097  simp3rl  1101  rmob  3145  elpr2elpr  3901  disjiun  4125  reg3exmidlemwe  4728  opabssxpd  4813  0xp  4857  imainss  5206  iotam  5372  fvmptt  5800  fcof1o  5998  isotr  6025  riota5f  6068  ovmpodf  6223  unielxp  6412  fnmpoovd  6455  1stconst  6461  2ndconst  6462  cnvf1olem  6464  fvn0elsupp  6495  suppcofn  6510  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemres  6624  tfrcllemres  6637  tfrcldm  6638  frecabcl  6674  nnaordi  6785  swoer  6839  qliftfun  6895  ecopovsymg  6912  th3qlem1  6915  pw2f1odclem  7139  mapen  7151  mapxpen  7153  fidifsnen  7177  fisbth  7192  findcard2d  7200  findcard2sd  7201  diffisn  7202  diffifi  7203  ac6sfi  7207  fidcen  7208  fimax2gtri  7211  fientri3  7227  nnwetri  7228  unsnfi  7231  unsnfidcex  7232  unsnfidcel  7233  fisseneq  7247  exmidssfi  7251  fidcenumlemrk  7277  fidcenumlemr  7278  isbth  7290  ordiso2  7382  difinfsnlem  7446  difinfinf  7448  ctmlemr  7455  ctssdccl  7458  fodjum  7493  fodju0  7494  omniwomnimkv  7514  exmidfodomrlemrALT  7562  netap  7627  exmidmotap  7634  cc1  7638  cc2lem  7639  cc3  7641  cc4f  7642  cc4n  7644  dfplpq2  7728  dfmpq2  7729  mulpipqqs  7747  distrnqg  7761  ltexnqq  7782  subhalfnqq  7788  distrnq0  7833  prarloclemup  7869  prarloclem3  7871  prarloc  7877  genplt2i  7884  nqprl  7925  nqpru  7926  prmuloc  7940  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltaddpr  7971  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  ltaprlem  7992  ltaprg  7993  prplnqu  7994  addextpr  7995  recexprlemdisj  8004  recexprlemloc  8005  recexprlem1ssl  8007  aptiprleml  8013  aptiprlemu  8014  ltmprr  8016  archpr  8017  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlem1  8033  cauappcvgprlem2  8034  cauappcvgprlemlim  8035  caucvgprlemnkj  8040  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprlem2  8054  caucvgprprlemnkltj  8063  caucvgprprlemnkeqj  8064  caucvgprprlemnjltk  8065  caucvgprprlemmu  8069  caucvgprprlemopl  8071  caucvgprprlemopu  8073  caucvgprprlemdisj  8076  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemaddq  8082  caucvgprprlem2  8084  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemex  8096  suplocexprlemub  8097  suplocexprlemlub  8098  recexgt0sr  8147  mulgt0sr  8152  prsrriota  8162  caucvgsrlemoffres  8174  suplocsrlem  8182  cnm  8206  addcnsr  8208  mulcnsr  8209  mulcnsrec  8217  axaddcl  8238  axmulcl  8240  axmulcom  8245  rereceu  8263  recriota  8264  axcaucvglemres  8273  axpre-suploclemres  8275  lelttr  8421  ltletr  8422  readdcan  8474  addcan  8514  addcan2  8515  addsub4  8577  ltadd2  8755  le2add  8780  lt2add  8781  lt2sub  8796  le2sub  8797  eqord1  8819  rimul  8922  rereim  8923  ltmul1  8929  apreim  8940  mulreim  8941  apcotr  8944  apadd1  8945  addext  8947  apneg  8948  mulext1  8949  mulext  8951  ltleap  8969  aprcl  8983  mulap0  8991  mulcanapd  8998  receuap  9008  recapb  9010  rec11ap  9049  rec11rap  9050  divdivdivap  9052  ddcanap  9065  divadddivap  9066  conjmulap  9068  subrecap  9178  prodgt0gt0  9190  prodge0  9193  ltmul12a  9199  lemulge11  9205  lt2mul2div  9218  ltrec  9222  lerec  9223  lt2msq  9225  lerec2  9228  le2msq  9240  msq11  9241  ledivp1  9242  mulle0r  9283  suprzclex  9756  peano5uzti  9766  supinfneg  10012  infsupneg  10013  qapne  10056  xrlelttr  10226  xrltletr  10227  xrre  10240  xaddge0  10298  xle2add  10299  xlt2add  10300  divelunit  10422  fzass4  10486  fzocatel  10635  zsupcllemstep  10680  zssinfcl  10683  infssfzcldc  10687  infssfzledc  10688  suprzubdc  10689  zsupssdc  10691  suprzcl2dc  10692  exbtwnzlemex  10702  rebtwn2z  10707  qbtwnre  10709  modqid  10808  modqcyc  10818  modqaddabs  10821  modqaddmod  10822  mulqaddmodid  10823  modqadd2mod  10833  modqltm1p1mod  10835  modqsubmod  10841  modqsubmodmod  10842  modqmulmod  10848  modqmulmodr  10849  modqaddmulmod  10850  modqsubdir  10852  frec2uzisod  10866  iseqovex  10917  seqvalcd  10920  seq1g  10922  seqf  10923  seqovcd  10926  seqm1g  10933  seq3fveq2  10934  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  iseqf1olemnab  10960  seqf1oglem1  10978  seqf1og  10980  seq3id2  10985  seqhomog  10989  seq3distr  10991  expcl2lemap  11010  expnegzap  11032  ltexp2a  11050  le2sq2  11074  nn0ltexp2  11170  nn0opth2  11185  bcval5  11224  hashcl  11243  hashen  11246  fihashdom  11266  hashunlem  11267  hashun  11268  hashmap  11291  fimaxq  11293  hashfibclem  11305  hashfibc  11306  hashf1lem1  11308  hashf1lem2  11309  hashf1  11310  zfz1isolem1  11315  zfz1iso  11316  lencl  11331  sswrd  11336  fstwrdne0  11367  lswlgt0cl  11380  ccatw2s1p1g  11436  ccat2s1fstg  11439  swrdval  11443  wrdind  11517  wrd2ind  11518  swrdccatfn  11519  swrdccatin1  11520  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12  11528  pfxccat3a  11533  reuccatpfxs1  11542  cvg1nlemres  11774  cvg1n  11775  recvguniq  11784  resqrexlemp1rp  11795  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemex  11814  sqrtmul  11824  sqrtsq  11833  absexpzap  11870  absle  11879  abs3lem  11901  amgm2  11908  maxleastlt  12005  maxltsup  12008  fimaxre2  12017  fiidxsupcl  12019  xrmaxleastlt  12048  xrmaxltsup  12050  xrmaxaddlem  12052  climcn2  12101  addcn2  12102  mulcn2  12104  reccn2ap  12105  climcau  12139  summodclem2  12175  summodc  12176  fsumf1o  12183  fisumss  12185  fsum3cvg3  12189  fsumcl2lem  12191  fsumadd  12199  fsum2dlemstep  12227  mptfzshft  12235  fsumrev  12236  fsummulc2  12241  modfsummod  12251  fsumrelem  12264  binom  12277  cvgratnn  12324  mertenslemub  12327  prodmodc  12371  zproddc  12372  fprodf1o  12381  fprodssdc  12383  fprodmul  12384  fprodrev  12412  fprod2dlemstep  12415  efcllem  12452  tanaddaplem  12531  dvdsval2  12583  moddvds  12592  dvdsabseq  12640  dvdsflip  12644  oexpneg  12670  fldivndvdslt  12730  bitsfi  12750  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemeu  12810  dfgcd3  12813  bezout  12814  dvdsmulgcd  12828  bezoutr  12835  nninfctlemfo  12843  ialgrlem1st  12846  lcmgcdlem  12881  coprmdvds2  12897  qredeu  12901  rpdvds  12903  isprm5lem  12946  isprm6  12952  pwbdvdslemn  12970  nnmaxpwlemparts  12978  nonsq  13013  crth  13032  eulerthlemh  13039  pclemdc  13097  pcprendvds2  13100  pceu  13104  pcval  13105  pczpre  13106  pcmul  13110  pcqmul  13112  pcqcl  13115  pcid  13133  pcneg  13134  pcgcd1  13137  pc2dvds  13139  pcprmpw2  13142  difsqpwdvds  13147  pcmpt  13152  pockthg  13166  1arith  13176  mul4sq  13203  4sqexercise2  13208  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemg  13353  ennnfonelemex  13364  ennnfonelemrnh  13366  ennnfonelemrn  13369  ennnfonelemdm  13370  ennnfonelemnn0  13372  ennnfonelemim  13374  ennnfone  13375  ctinfomlemom  13377  ctinf  13380  ctiunctlemfo  13389  nninfdclemcl  13398  nninfdclemf  13399  nninfdclemp1  13400  unbendc  13404  isstruct2r  13422  setscom  13451  qusval  13704  ercpbl  13712  opifismgmdc  13751  grpinvalem  13765  grprida  13767  gzsumvalx  13769  gzsumfzval  13771  gzsumval2  13774  sgrppropd  13788  mndpropd  13813  issubmnd  13815  submnd0  13817  mhmf1o  13837  0mhm  13853  resmhm  13854  mhmco  13857  mhmima  13858  mhmeql  13859  gzsumwsubmcl  13861  gzsumcl  13864  grppropd  13882  grpinvid1  13917  grpinvid2  13918  grplcan  13927  grplmulf1o  13939  grpnpncan0  13961  dfgrp3mlem  13963  grplactcnv  13967  mulgval  13985  mulgfng  13987  mulg1  13992  mulgnnp1  13993  mulgneg  14003  mulgnndir  14014  mulgdirlem  14016  mulgnn0ass  14021  mulgass  14022  subgmulg  14051  issubg4m  14056  subgintm  14061  0nsg  14077  eqgcpbl  14091  ghmmulg  14119  ghmpreima  14129  ghmeql  14130  ghmnsgima  14131  ghmnsgpreima  14132  ghmf1  14136  ghmf1o  14138  conjghm  14139  conjnmzb  14143  qusghm  14145  cntzsgrpcl  14168  cntzsubm  14171  cntzsubg  14172  cntrsubgnsg  14176  cmnsubm  14203  ablpncan3  14212  invghm  14224  eqgabl  14225  qusecsub  14226  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gsumvalfi  14243  gsumclfi  14250  gsummptfidmadd  14252  gsumsubmclfi  14254  gsummptfidmsplit  14255  gsumresfi  14264  gsum2dfilem2  14273  gsum2d2fi  14275  prdssgrpd  14299  prdsmndd  14302  pwssub  14324  imasrng  14363  qusrng  14365  srglmhm  14405  srgrmhm  14406  ringpropd  14451  ringlghm  14474  ringrghm  14475  imasring  14479  qusring2  14481  opprrngbg  14493  dvdsrvald  14510  dvdsrd  14511  dvdsrex  14515  dvdsrtr  14518  unitgrp  14533  unitpropdg  14565  rhmopp  14593  isnzr2  14601  issubrng2  14628  subrngintm  14630  subrgintm  14661  rhmpropd  14672  ringunitap  14703  aprap  14708  drngunitap  14718  lmodprop2d  14795  rmodislmodlem  14797  lssvacl  14812  lssvsubcl  14813  lssvscl  14822  islss3  14826  lsspropdg  14878  rnglidlmcl  14927  2idlcpblrng  14970  crngridl  14977  gsumfsum  15033  expghmap  15052  mulgghm2  15053  mulgrhm  15054  znf1o  15096  znleval  15098  znidom  15102  issubassa3  15122  assapropd  15124  asclghm  15135  issubassa2  15145  psrval  15162  psrbagcon  15176  psrbaglefifi  15177  psrbagconf1o  15179  gsumbagdiaglem  15180  gsumbagdiagfi  15181  psrass1filem  15182  mplsubgfilemcl  15227  epttop  15328  topssnei  15400  restbasg  15406  restopnb  15419  cnfval  15432  cnpfval  15433  iscnp4  15456  cnpnei  15457  cnptopco  15460  cncnp  15468  cnrest2  15474  cnptoprest  15477  cnptoprest2  15478  lmss  15484  lmtopcnp  15488  neitx  15506  txcnp  15509  txrest  15514  txdis  15515  txlm  15517  cnmpt21  15529  imasnopn  15537  xmetres2  15617  blvalps  15626  blval  15627  bl2in  15641  blhalf  15646  blssps  15665  blss  15666  blssexps  15667  blssex  15668  ssblex  15669  blin2  15670  metss2lem  15735  bdmetval  15738  bdmopn  15742  metrest  15744  xmetxp  15745  xmetxpbl  15746  xmettx  15748  metcnp3  15749  txmetcnp  15756  addcncntoplem  15799  elcncf2  15812  mulc1cncf  15827  cncfco  15829  cncfmet  15830  mulcncf  15846  dedekindeulemub  15856  dedekindeulemloc  15857  dedekindeulemlu  15859  dedekindeu  15861  suplociccex  15863  dedekindicclemub  15865  dedekindicclemloc  15866  dedekindicclemlu  15868  dedekindicc  15871  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthdec  15882  ivthreinc  15883  dich0  15890  limcimolemlt  15902  limcimo  15903  cnplimccntop  15908  limccnp2lem  15914  limccnp2cntop  15915  dvfvalap  15919  dvmptfsum  15963  dveflem  15964  plyco  15997  plycn  16000  plyrecj  16001  reeff1olem  16009  reeff1oleme  16010  eflt  16013  sin0pilem2  16021  pilem3  16022  ptolemy  16063  ioocosf1o  16094  logdivlt  16136  logdivle  16137  rpcxpmul2z  16160  cxplt  16163  cxple  16164  cxplt3  16167  apcxp2  16186  rprelogbmul  16203  rprelogbdiv  16205  logbgt0b  16214  logbgcd1irrap  16218  zprmlogbap  16230  pellexlem3  16243  efnnfsumcl  16251  ppinprm  16272  chtnprm  16274  efchtqdvds  16277  fsumdvdsmul  16297  chtublem  16307  perfectlem2  16312  bposlem3  16325  lgsdir2lem5  16368  lgsdir  16371  lgsdi  16373  lgsne0  16374  gausslemma2dlem1f1o  16396  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem2  16418  lgsquad2  16419  2sqlem6  16456  2sqlem10  16461  upgredg  16602  uhgrissubgr  16719  subgrprop3  16720  upgrspanop  16741  umgrspanop  16742  usgrspanop  16743  vtxedgfi  16747  vtxlpfi  16748  upgr2wlkdc  16835  clwwlkccatlem  16858  eupth2lemsfi  16936  depindlem3  16966  nnti  17239  pwtrufal  17244  pwf1oexmid  17246  sssneq  17249  qdencn  17290  cvgcmp2n  17300  trilpolemlt1  17309  trirec0  17312  trirec0xor  17313  qdiff  17317  redc0  17326  reap0  17327  cndcap  17328  nconstwlpolemgt0  17333  neap0mkv  17338  supfz  17340  inffz  17341