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

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  994  simp1rl  1093  simp2rl  1097  simp3rl  1101  rmob  3145  elpr2elpr  3899  disjiun  4123  reg3exmidlemwe  4724  opabssxpd  4809  0xp  4853  imainss  5201  iotam  5367  fvmptt  5794  fcof1o  5989  isotr  6016  riota5f  6059  ovmpodf  6214  unielxp  6402  fnmpoovd  6445  1stconst  6451  2ndconst  6452  cnvf1olem  6454  fvn0elsupp  6485  suppcofn  6500  tfrlemi14d  6598  tfrexlem  6599  tfr1onlemres  6614  tfrcllemres  6627  tfrcldm  6628  frecabcl  6664  nnaordi  6775  swoer  6829  qliftfun  6885  ecopovsymg  6902  th3qlem1  6905  pw2f1odclem  7128  mapen  7140  mapxpen  7142  fidifsnen  7166  fisbth  7181  findcard2d  7189  findcard2sd  7190  diffisn  7191  diffifi  7192  ac6sfi  7196  fidcen  7197  fimax2gtri  7200  fientri3  7216  nnwetri  7217  unsnfi  7220  unsnfidcex  7221  unsnfidcel  7222  fisseneq  7236  exmidssfi  7240  fidcenumlemrk  7265  fidcenumlemr  7266  isbth  7278  ordiso2  7369  difinfsnlem  7433  difinfinf  7435  ctmlemr  7442  ctssdccl  7445  fodjum  7480  fodju0  7481  omniwomnimkv  7501  exmidfodomrlemrALT  7549  netap  7614  exmidmotap  7621  cc1  7625  cc2lem  7626  cc3  7628  cc4f  7629  cc4n  7631  dfplpq2  7715  dfmpq2  7716  mulpipqqs  7734  distrnqg  7748  ltexnqq  7769  subhalfnqq  7775  distrnq0  7820  prarloclemup  7856  prarloclem3  7858  prarloc  7864  genplt2i  7871  nqprl  7912  nqpru  7913  prmuloc  7927  mullocpr  7932  distrlem4prl  7945  distrlem4pru  7946  ltaddpr  7958  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  ltaprlem  7979  ltaprg  7980  prplnqu  7981  addextpr  7982  recexprlemdisj  7991  recexprlemloc  7992  recexprlem1ssl  7994  aptiprleml  8000  aptiprlemu  8001  ltmprr  8003  archpr  8004  cauappcvgprlemopl  8007  cauappcvgprlemopu  8009  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlem1  8020  cauappcvgprlem2  8021  cauappcvgprlemlim  8022  caucvgprlemnkj  8027  caucvgprlemopl  8030  caucvgprlemopu  8032  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprlem2  8041  caucvgprprlemnkltj  8050  caucvgprprlemnkeqj  8051  caucvgprprlemnjltk  8052  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemopu  8060  caucvgprprlemdisj  8063  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  caucvgprprlemaddq  8069  caucvgprprlem2  8071  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemex  8083  suplocexprlemub  8084  suplocexprlemlub  8085  recexgt0sr  8134  mulgt0sr  8139  prsrriota  8149  caucvgsrlemoffres  8161  suplocsrlem  8169  cnm  8193  addcnsr  8195  mulcnsr  8196  mulcnsrec  8204  axaddcl  8225  axmulcl  8227  axmulcom  8232  rereceu  8250  recriota  8251  axcaucvglemres  8260  axpre-suploclemres  8262  lelttr  8408  ltletr  8409  readdcan  8460  addcan  8500  addcan2  8501  addsub4  8563  ltadd2  8741  le2add  8766  lt2add  8767  lt2sub  8782  le2sub  8783  eqord1  8805  rimul  8907  rereim  8908  ltmul1  8914  apreim  8925  mulreim  8926  apcotr  8929  apadd1  8930  addext  8932  apneg  8933  mulext1  8934  mulext  8936  ltleap  8954  aprcl  8968  mulap0  8976  mulcanapd  8983  receuap  8993  recapb  8995  rec11ap  9034  rec11rap  9035  divdivdivap  9037  ddcanap  9050  divadddivap  9051  conjmulap  9053  subrecap  9163  prodgt0gt0  9175  prodge0  9178  ltmul12a  9184  lemulge11  9190  lt2mul2div  9203  ltrec  9207  lerec  9208  lt2msq  9210  lerec2  9213  le2msq  9225  msq11  9226  ledivp1  9227  mulle0r  9268  suprzclex  9727  peano5uzti  9737  supinfneg  9978  infsupneg  9979  qapne  10022  xrlelttr  10191  xrltletr  10192  xrre  10205  xaddge0  10263  xle2add  10264  xlt2add  10265  divelunit  10387  fzass4  10451  fzocatel  10600  zsupcllemstep  10645  zssinfcl  10648  infssfzcldc  10652  infssfzledc  10653  suprzubdc  10654  zsupssdc  10656  suprzcl2dc  10657  exbtwnzlemex  10667  rebtwn2z  10672  qbtwnre  10674  modqid  10769  modqcyc  10779  modqaddabs  10782  modqaddmod  10783  mulqaddmodid  10784  modqadd2mod  10794  modqltm1p1mod  10796  modqsubmod  10802  modqsubmodmod  10803  modqmulmod  10809  modqmulmodr  10810  modqaddmulmod  10811  modqsubdir  10813  frec2uzisod  10827  iseqovex  10878  seqvalcd  10881  seq1g  10883  seqf  10884  seqovcd  10887  seqm1g  10894  seq3fveq2  10895  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  iseqf1olemnab  10921  seqf1oglem1  10939  seqf1og  10941  seq3id2  10946  seqhomog  10950  seq3distr  10952  expcl2lemap  10971  expnegzap  10993  ltexp2a  11011  le2sq2  11035  nn0ltexp2  11130  nn0opth2  11145  bcval5  11184  hashcl  11203  hashen  11206  fihashdom  11226  hashunlem  11227  hashun  11228  hashmap  11251  fimaxq  11253  hashfibclem  11265  hashfibc  11266  hashf1lem1  11268  hashf1lem2  11269  hashf1  11270  zfz1isolem1  11275  zfz1iso  11276  lencl  11291  sswrd  11296  fstwrdne0  11327  lswlgt0cl  11340  ccatw2s1p1g  11396  ccat2s1fstg  11399  swrdval  11403  wrdind  11477  wrd2ind  11478  swrdccatfn  11479  swrdccatin1  11480  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12  11488  pfxccat3a  11493  reuccatpfxs1  11502  cvg1nlemres  11734  cvg1n  11735  recvguniq  11744  resqrexlemp1rp  11755  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemex  11774  sqrtmul  11784  sqrtsq  11793  absexpzap  11829  absle  11838  abs3lem  11860  amgm2  11867  maxleastlt  11964  maxltsup  11967  fimaxre2  11976  xrmaxleastlt  12005  xrmaxltsup  12007  xrmaxaddlem  12009  climcn2  12058  addcn2  12059  mulcn2  12061  reccn2ap  12062  climcau  12096  summodclem2  12132  summodc  12133  fsumf1o  12140  fisumss  12142  fsum3cvg3  12146  fsumcl2lem  12148  fsumadd  12156  fsum2dlemstep  12184  mptfzshft  12192  fsumrev  12193  fsummulc2  12198  modfsummod  12208  fsumrelem  12221  binom  12234  cvgratnn  12281  mertenslemub  12284  prodmodc  12328  zproddc  12329  fprodf1o  12338  fprodssdc  12340  fprodmul  12341  fprodrev  12369  fprod2dlemstep  12372  efcllem  12409  tanaddaplem  12488  dvdsval2  12540  moddvds  12549  dvdsabseq  12597  dvdsflip  12601  oexpneg  12627  fldivndvdslt  12687  bitsfi  12707  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemeu  12767  dfgcd3  12770  bezout  12771  dvdsmulgcd  12785  bezoutr  12792  nninfctlemfo  12800  ialgrlem1st  12803  lcmgcdlem  12838  coprmdvds2  12854  qredeu  12858  rpdvds  12860  isprm5lem  12902  isprm6  12908  pw2dvdslemn  12926  nonsq  12968  crth  12985  eulerthlemh  12992  pclemdc  13050  pcprendvds2  13053  pceu  13057  pcval  13058  pczpre  13059  pcmul  13063  pcqmul  13065  pcqcl  13068  pcid  13086  pcneg  13087  pcgcd1  13090  pc2dvds  13092  pcprmpw2  13095  difsqpwdvds  13100  pcmpt  13105  pockthg  13119  1arith  13129  mul4sq  13156  4sqexercise2  13161  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemg  13277  ennnfonelemex  13288  ennnfonelemrnh  13290  ennnfonelemrn  13293  ennnfonelemdm  13294  ennnfonelemnn0  13296  ennnfonelemim  13298  ennnfone  13299  ctinfomlemom  13301  ctinf  13304  ctiunctlemfo  13313  nninfdclemcl  13322  nninfdclemf  13323  nninfdclemp1  13324  unbendc  13328  isstruct2r  13346  setscom  13375  qusval  13627  ercpbl  13635  opifismgmdc  13674  grpinvalem  13688  grprida  13690  gzsumvalx  13692  gzsumfzval  13694  gzsumval2  13697  sgrppropd  13711  mndpropd  13736  issubmnd  13738  submnd0  13740  mhmf1o  13760  0mhm  13776  resmhm  13777  mhmco  13780  mhmima  13781  mhmeql  13782  gzsumwsubmcl  13784  gzsumcl  13787  grppropd  13805  grpinvid1  13840  grpinvid2  13841  grplcan  13850  grplmulf1o  13862  grpnpncan0  13884  dfgrp3mlem  13886  grplactcnv  13890  mulgval  13908  mulgfng  13910  mulg1  13915  mulgnnp1  13916  mulgneg  13926  mulgnndir  13937  mulgdirlem  13939  mulgnn0ass  13944  mulgass  13945  subgmulg  13974  issubg4m  13979  subgintm  13984  0nsg  14000  eqgcpbl  14014  ghmmulg  14042  ghmpreima  14052  ghmeql  14053  ghmnsgima  14054  ghmnsgpreima  14055  ghmf1  14059  ghmf1o  14061  conjghm  14062  conjnmzb  14066  qusghm  14068  cmnsubm  14095  ablpncan3  14104  invghm  14116  eqgabl  14117  qusecsub  14118  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gsumvalfi  14135  gsumclfi  14142  gsummptfidmadd  14144  gsumsubmclfi  14146  prdssgrpd  14174  prdsmndd  14177  pwssub  14199  imasrng  14238  qusrng  14240  srglmhm  14280  srgrmhm  14281  ringpropd  14326  ringlghm  14349  ringrghm  14350  imasring  14352  qusring2  14354  opprrngbg  14366  dvdsrvald  14383  dvdsrd  14384  dvdsrex  14388  dvdsrtr  14391  unitgrp  14406  unitpropdg  14438  rhmopp  14466  isnzr2  14474  issubrng2  14501  subrngintm  14503  subrgintm  14534  rhmpropd  14545  ringunitap  14576  aprap  14581  drngunitap  14591  lmodprop2d  14668  rmodislmodlem  14670  lssvacl  14685  lssvsubcl  14686  lssvscl  14695  islss3  14699  lsspropdg  14751  rnglidlmcl  14800  2idlcpblrng  14843  crngridl  14850  gsumfsum  14906  expghmap  14925  mulgghm2  14926  mulgrhm  14927  znf1o  14969  znleval  14971  znidom  14975  issubassa3  14995  assapropd  14997  asclghm  15008  issubassa2  15018  psrval  15033  psrbagcon  15045  psrbagconf1o  15047  mplsubgfilemcl  15073  epttop  15174  topssnei  15246  restbasg  15252  restopnb  15265  cnfval  15278  cnpfval  15279  iscnp4  15302  cnpnei  15303  cnptopco  15306  cncnp  15314  cnrest2  15320  cnptoprest  15323  cnptoprest2  15324  lmss  15330  lmtopcnp  15334  neitx  15352  txcnp  15355  txrest  15360  txdis  15361  txlm  15363  cnmpt21  15375  imasnopn  15383  xmetres2  15463  blvalps  15472  blval  15473  bl2in  15487  blhalf  15492  blssps  15511  blss  15512  blssexps  15513  blssex  15514  ssblex  15515  blin2  15516  metss2lem  15581  bdmetval  15584  bdmopn  15588  metrest  15590  xmetxp  15591  xmetxpbl  15592  xmettx  15594  metcnp3  15595  txmetcnp  15602  addcncntoplem  15645  elcncf2  15658  mulc1cncf  15673  cncfco  15675  cncfmet  15676  mulcncf  15692  dedekindeulemub  15702  dedekindeulemloc  15703  dedekindeulemlu  15705  dedekindeu  15707  suplociccex  15709  dedekindicclemub  15711  dedekindicclemloc  15712  dedekindicclemlu  15714  dedekindicc  15717  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthdec  15728  ivthreinc  15729  dich0  15736  limcimolemlt  15748  limcimo  15749  cnplimccntop  15754  limccnp2lem  15760  limccnp2cntop  15761  dvfvalap  15765  dvmptfsum  15809  dveflem  15810  plyco  15843  plycn  15846  plyrecj  15847  reeff1olem  15855  reeff1oleme  15856  eflt  15859  sin0pilem2  15866  pilem3  15867  ptolemy  15908  ioocosf1o  15938  cxplt  16001  cxple  16002  cxplt3  16005  apcxp2  16024  rprelogbmul  16040  rprelogbdiv  16042  logbgt0b  16051  logbgcd1irrap  16055  pellexlem3  16076  fsumdvdsmul  16088  perfectlem2  16097  lgsdir2lem5  16134  lgsdir  16137  lgsdi  16139  lgsne0  16140  gausslemma2dlem1f1o  16162  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem2  16184  lgsquad2  16185  2sqlem6  16222  2sqlem10  16227  upgredg  16368  uhgrissubgr  16485  subgrprop3  16486  upgrspanop  16507  umgrspanop  16508  usgrspanop  16509  vtxedgfi  16513  vtxlpfi  16514  upgr2wlkdc  16601  clwwlkccatlem  16624  eupth2lemsfi  16702  depindlem3  16732  nnti  17005  pwtrufal  17010  pwf1oexmid  17012  sssneq  17015  qdencn  17046  cvgcmp2n  17056  trilpolemlt1  17064  trirec0  17067  trirec0xor  17068  qdiff  17072  redc0  17081  reap0  17082  cndcap  17083  nconstwlpolemgt0  17088  neap0mkv  17093  supfz  17095  inffz  17096