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  4726  opabssxpd  4811  0xp  4855  imainss  5203  iotam  5369  fvmptt  5797  fcof1o  5995  isotr  6022  riota5f  6065  ovmpodf  6220  unielxp  6408  fnmpoovd  6451  1stconst  6457  2ndconst  6458  cnvf1olem  6460  fvn0elsupp  6491  suppcofn  6506  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  frecabcl  6670  nnaordi  6781  swoer  6835  qliftfun  6891  ecopovsymg  6908  th3qlem1  6911  pw2f1odclem  7134  mapen  7146  mapxpen  7148  fidifsnen  7172  fisbth  7187  findcard2d  7195  findcard2sd  7196  diffisn  7197  diffifi  7198  ac6sfi  7202  fidcen  7203  fimax2gtri  7206  fientri3  7222  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  exmidssfi  7246  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  ordiso2  7375  difinfsnlem  7439  difinfinf  7441  ctmlemr  7448  ctssdccl  7451  fodjum  7486  fodju0  7487  omniwomnimkv  7507  exmidfodomrlemrALT  7555  netap  7620  exmidmotap  7627  cc1  7631  cc2lem  7632  cc3  7634  cc4f  7635  cc4n  7637  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  ltexnqq  7775  subhalfnqq  7781  distrnq0  7826  prarloclemup  7862  prarloclem3  7864  prarloc  7870  genplt2i  7877  nqprl  7918  nqpru  7919  prmuloc  7933  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltaddpr  7964  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprlem  7985  ltaprg  7986  prplnqu  7987  addextpr  7988  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  recexgt0sr  8140  mulgt0sr  8145  prsrriota  8155  caucvgsrlemoffres  8167  suplocsrlem  8175  cnm  8199  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axaddcl  8231  axmulcl  8233  axmulcom  8238  rereceu  8256  recriota  8257  axcaucvglemres  8266  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  readdcan  8466  addcan  8506  addcan2  8507  addsub4  8569  ltadd2  8747  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  eqord1  8811  rimul  8914  rereim  8915  ltmul1  8921  apreim  8932  mulreim  8933  apcotr  8936  apadd1  8937  addext  8939  apneg  8940  mulext1  8941  mulext  8943  ltleap  8961  aprcl  8975  mulap0  8983  mulcanapd  8990  receuap  9000  recapb  9002  rec11ap  9041  rec11rap  9042  divdivdivap  9044  ddcanap  9057  divadddivap  9058  conjmulap  9060  subrecap  9170  prodgt0gt0  9182  prodge0  9185  ltmul12a  9191  lemulge11  9197  lt2mul2div  9210  ltrec  9214  lerec  9215  lt2msq  9217  lerec2  9220  le2msq  9232  msq11  9233  ledivp1  9234  mulle0r  9275  suprzclex  9746  peano5uzti  9756  supinfneg  9997  infsupneg  9998  qapne  10041  xrlelttr  10210  xrltletr  10211  xrre  10224  xaddge0  10282  xle2add  10283  xlt2add  10284  divelunit  10406  fzass4  10470  fzocatel  10619  zsupcllemstep  10664  zssinfcl  10667  infssfzcldc  10671  infssfzledc  10672  suprzubdc  10673  zsupssdc  10675  suprzcl2dc  10676  exbtwnzlemex  10686  rebtwn2z  10691  qbtwnre  10693  modqid  10788  modqcyc  10798  modqaddabs  10801  modqaddmod  10802  mulqaddmodid  10803  modqadd2mod  10813  modqltm1p1mod  10815  modqsubmod  10821  modqsubmodmod  10822  modqmulmod  10828  modqmulmodr  10829  modqaddmulmod  10830  modqsubdir  10832  frec2uzisod  10846  iseqovex  10897  seqvalcd  10900  seq1g  10902  seqf  10903  seqovcd  10906  seqm1g  10913  seq3fveq2  10914  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  iseqf1olemnab  10940  seqf1oglem1  10958  seqf1og  10960  seq3id2  10965  seqhomog  10969  seq3distr  10971  expcl2lemap  10990  expnegzap  11012  ltexp2a  11030  le2sq2  11054  nn0ltexp2  11149  nn0opth2  11164  bcval5  11203  hashcl  11222  hashen  11225  fihashdom  11245  hashunlem  11246  hashun  11247  hashmap  11270  fimaxq  11272  hashfibclem  11284  hashfibc  11285  hashf1lem1  11287  hashf1lem2  11288  hashf1  11289  zfz1isolem1  11294  zfz1iso  11295  lencl  11310  sswrd  11315  fstwrdne0  11346  lswlgt0cl  11359  ccatw2s1p1g  11415  ccat2s1fstg  11418  swrdval  11422  wrdind  11496  wrd2ind  11497  swrdccatfn  11498  swrdccatin1  11499  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12  11507  pfxccat3a  11512  reuccatpfxs1  11521  cvg1nlemres  11753  cvg1n  11754  recvguniq  11763  resqrexlemp1rp  11774  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemex  11793  sqrtmul  11803  sqrtsq  11812  absexpzap  11848  absle  11857  abs3lem  11879  amgm2  11886  maxleastlt  11983  maxltsup  11986  fimaxre2  11995  xrmaxleastlt  12024  xrmaxltsup  12026  xrmaxaddlem  12028  climcn2  12077  addcn2  12078  mulcn2  12080  reccn2ap  12081  climcau  12115  summodclem2  12151  summodc  12152  fsumf1o  12159  fisumss  12161  fsum3cvg3  12165  fsumcl2lem  12167  fsumadd  12175  fsum2dlemstep  12203  mptfzshft  12211  fsumrev  12212  fsummulc2  12217  modfsummod  12227  fsumrelem  12240  binom  12253  cvgratnn  12300  mertenslemub  12303  prodmodc  12347  zproddc  12348  fprodf1o  12357  fprodssdc  12359  fprodmul  12360  fprodrev  12388  fprod2dlemstep  12391  efcllem  12428  tanaddaplem  12507  dvdsval2  12559  moddvds  12568  dvdsabseq  12616  dvdsflip  12620  oexpneg  12646  fldivndvdslt  12706  bitsfi  12726  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemeu  12786  dfgcd3  12789  bezout  12790  dvdsmulgcd  12804  bezoutr  12811  nninfctlemfo  12819  ialgrlem1st  12822  lcmgcdlem  12857  coprmdvds2  12873  qredeu  12877  rpdvds  12879  isprm5lem  12921  isprm6  12927  pw2dvdslemn  12945  nonsq  12987  crth  13004  eulerthlemh  13011  pclemdc  13069  pcprendvds2  13072  pceu  13076  pcval  13077  pczpre  13078  pcmul  13082  pcqmul  13084  pcqcl  13087  pcid  13105  pcneg  13106  pcgcd1  13109  pc2dvds  13111  pcprmpw2  13114  difsqpwdvds  13119  pcmpt  13124  pockthg  13138  1arith  13148  mul4sq  13175  4sqexercise2  13180  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemg  13296  ennnfonelemex  13307  ennnfonelemrnh  13309  ennnfonelemrn  13312  ennnfonelemdm  13313  ennnfonelemnn0  13315  ennnfonelemim  13317  ennnfone  13318  ctinfomlemom  13320  ctinf  13323  ctiunctlemfo  13332  nninfdclemcl  13341  nninfdclemf  13342  nninfdclemp1  13343  unbendc  13347  isstruct2r  13365  setscom  13394  qusval  13646  ercpbl  13654  opifismgmdc  13693  grpinvalem  13707  grprida  13709  gzsumvalx  13711  gzsumfzval  13713  gzsumval2  13716  sgrppropd  13730  mndpropd  13755  issubmnd  13757  submnd0  13759  mhmf1o  13779  0mhm  13795  resmhm  13796  mhmco  13799  mhmima  13800  mhmeql  13801  gzsumwsubmcl  13803  gzsumcl  13806  grppropd  13824  grpinvid1  13859  grpinvid2  13860  grplcan  13869  grplmulf1o  13881  grpnpncan0  13903  dfgrp3mlem  13905  grplactcnv  13909  mulgval  13927  mulgfng  13929  mulg1  13934  mulgnnp1  13935  mulgneg  13945  mulgnndir  13956  mulgdirlem  13958  mulgnn0ass  13963  mulgass  13964  subgmulg  13993  issubg4m  13998  subgintm  14003  0nsg  14019  eqgcpbl  14033  ghmmulg  14061  ghmpreima  14071  ghmeql  14072  ghmnsgima  14073  ghmnsgpreima  14074  ghmf1  14078  ghmf1o  14080  conjghm  14081  conjnmzb  14085  qusghm  14087  cmnsubm  14114  ablpncan3  14123  invghm  14135  eqgabl  14136  qusecsub  14137  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gsumvalfi  14154  gsumclfi  14161  gsummptfidmadd  14163  gsumsubmclfi  14165  prdssgrpd  14193  prdsmndd  14196  pwssub  14218  imasrng  14257  qusrng  14259  srglmhm  14299  srgrmhm  14300  ringpropd  14345  ringlghm  14368  ringrghm  14369  imasring  14371  qusring2  14373  opprrngbg  14385  dvdsrvald  14402  dvdsrd  14403  dvdsrex  14407  dvdsrtr  14410  unitgrp  14425  unitpropdg  14457  rhmopp  14485  isnzr2  14493  issubrng2  14520  subrngintm  14522  subrgintm  14553  rhmpropd  14564  ringunitap  14595  aprap  14600  drngunitap  14610  lmodprop2d  14687  rmodislmodlem  14689  lssvacl  14704  lssvsubcl  14705  lssvscl  14714  islss3  14718  lsspropdg  14770  rnglidlmcl  14819  2idlcpblrng  14862  crngridl  14869  gsumfsum  14925  expghmap  14944  mulgghm2  14945  mulgrhm  14946  znf1o  14988  znleval  14990  znidom  14994  issubassa3  15014  assapropd  15016  asclghm  15027  issubassa2  15037  psrval  15052  psrbagcon  15064  psrbagconf1o  15066  mplsubgfilemcl  15092  epttop  15193  topssnei  15265  restbasg  15271  restopnb  15284  cnfval  15297  cnpfval  15298  iscnp4  15321  cnpnei  15322  cnptopco  15325  cncnp  15333  cnrest2  15339  cnptoprest  15342  cnptoprest2  15343  lmss  15349  lmtopcnp  15353  neitx  15371  txcnp  15374  txrest  15379  txdis  15380  txlm  15382  cnmpt21  15394  imasnopn  15402  xmetres2  15482  blvalps  15491  blval  15492  bl2in  15506  blhalf  15511  blssps  15530  blss  15531  blssexps  15532  blssex  15533  ssblex  15534  blin2  15535  metss2lem  15600  bdmetval  15603  bdmopn  15607  metrest  15609  xmetxp  15610  xmetxpbl  15611  xmettx  15613  metcnp3  15614  txmetcnp  15621  addcncntoplem  15664  elcncf2  15677  mulc1cncf  15692  cncfco  15694  cncfmet  15695  mulcncf  15711  dedekindeulemub  15721  dedekindeulemloc  15722  dedekindeulemlu  15724  dedekindeu  15726  suplociccex  15728  dedekindicclemub  15730  dedekindicclemloc  15731  dedekindicclemlu  15733  dedekindicc  15736  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthdec  15747  ivthreinc  15748  dich0  15755  limcimolemlt  15767  limcimo  15768  cnplimccntop  15773  limccnp2lem  15779  limccnp2cntop  15780  dvfvalap  15784  dvmptfsum  15828  dveflem  15829  plyco  15862  plycn  15865  plyrecj  15866  reeff1olem  15874  reeff1oleme  15875  eflt  15878  sin0pilem2  15886  pilem3  15887  ptolemy  15928  ioocosf1o  15958  logdivlt  15999  logdivle  16000  cxplt  16024  cxple  16025  cxplt3  16028  apcxp2  16047  rprelogbmul  16063  rprelogbdiv  16065  logbgt0b  16074  logbgcd1irrap  16078  pellexlem3  16099  fsumdvdsmul  16111  perfectlem2  16120  lgsdir2lem5  16163  lgsdir  16166  lgsdi  16168  lgsne0  16169  gausslemma2dlem1f1o  16191  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem2  16213  lgsquad2  16214  2sqlem6  16251  2sqlem10  16256  upgredg  16397  uhgrissubgr  16514  subgrprop3  16515  upgrspanop  16536  umgrspanop  16537  usgrspanop  16538  vtxedgfi  16542  vtxlpfi  16543  upgr2wlkdc  16630  clwwlkccatlem  16653  eupth2lemsfi  16731  depindlem3  16761  nnti  17034  pwtrufal  17039  pwf1oexmid  17041  sssneq  17044  qdencn  17084  cvgcmp2n  17094  trilpolemlt1  17102  trirec0  17105  trirec0xor  17106  qdiff  17110  redc0  17119  reap0  17120  cndcap  17121  nconstwlpolemgt0  17126  neap0mkv  17131  supfz  17133  inffz  17134