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  1062  simp2rl  1066  simp3rl  1070  rmob  3055  disjiun  3998  reg3exmidlemwe  4578  0xp  4706  imainss  5044  iotam  5208  fvmptt  5607  fcof1o  5789  isotr  5816  riota5f  5854  ovmpodf  6005  unielxp  6174  fnmpoovd  6215  1stconst  6221  2ndconst  6222  cnvf1olem  6224  tfrlemi14d  6333  tfrexlem  6334  tfr1onlemres  6349  tfrcllemres  6362  tfrcldm  6363  frecabcl  6399  nnaordi  6508  swoer  6562  qliftfun  6616  ecopovsymg  6633  th3qlem1  6636  mapen  6845  mapxpen  6847  fidifsnen  6869  fisbth  6882  findcard2d  6890  findcard2sd  6891  diffisn  6892  diffifi  6893  ac6sfi  6897  fimax2gtri  6900  fientri3  6913  nnwetri  6914  unsnfi  6917  unsnfidcex  6918  unsnfidcel  6919  fisseneq  6930  fidcenumlemrk  6952  fidcenumlemr  6953  isbth  6965  ordiso2  7033  difinfsnlem  7097  difinfinf  7099  ctmlemr  7106  ctssdccl  7109  fodjum  7143  fodju0  7144  omniwomnimkv  7164  exmidfodomrlemrALT  7201  netap  7252  exmidmotap  7259  cc1  7263  cc2lem  7264  cc3  7266  cc4f  7267  cc4n  7269  dfplpq2  7352  dfmpq2  7353  mulpipqqs  7371  distrnqg  7385  ltexnqq  7406  subhalfnqq  7412  distrnq0  7457  prarloclemup  7493  prarloclem3  7495  prarloc  7501  genplt2i  7508  nqprl  7549  nqpru  7550  prmuloc  7564  mullocpr  7569  distrlem4prl  7582  distrlem4pru  7583  ltaddpr  7595  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemrl  7608  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  ltaprlem  7616  ltaprg  7617  prplnqu  7618  addextpr  7619  recexprlemdisj  7628  recexprlemloc  7629  recexprlem1ssl  7631  aptiprleml  7637  aptiprlemu  7638  ltmprr  7640  archpr  7641  cauappcvgprlemopl  7644  cauappcvgprlemopu  7646  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlem1  7657  cauappcvgprlem2  7658  cauappcvgprlemlim  7659  caucvgprlemnkj  7664  caucvgprlemopl  7667  caucvgprlemopu  7669  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlem2  7678  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemnjltk  7689  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemopu  7697  caucvgprprlemdisj  7700  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  caucvgprprlem2  7708  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemex  7720  suplocexprlemub  7721  suplocexprlemlub  7722  recexgt0sr  7771  mulgt0sr  7776  prsrriota  7786  caucvgsrlemoffres  7798  suplocsrlem  7806  cnm  7830  addcnsr  7832  mulcnsr  7833  mulcnsrec  7841  axaddcl  7862  axmulcl  7864  axmulcom  7869  rereceu  7887  recriota  7888  axcaucvglemres  7897  axpre-suploclemres  7899  lelttr  8045  ltletr  8046  readdcan  8096  addcan  8136  addcan2  8137  addsub4  8199  ltadd2  8375  le2add  8400  lt2add  8401  lt2sub  8416  le2sub  8417  eqord1  8439  rimul  8541  rereim  8542  ltmul1  8548  apreim  8559  mulreim  8560  apcotr  8563  apadd1  8564  addext  8566  apneg  8567  mulext1  8568  mulext  8570  ltleap  8588  aprcl  8602  mulap0  8610  mulcanapd  8617  receuap  8625  recapb  8627  rec11ap  8666  rec11rap  8667  divdivdivap  8669  ddcanap  8682  divadddivap  8683  conjmulap  8685  subrecap  8795  prodgt0gt0  8807  prodge0  8810  ltmul12a  8816  lemulge11  8822  lt2mul2div  8835  ltrec  8839  lerec  8840  lt2msq  8842  lerec2  8845  le2msq  8857  msq11  8858  ledivp1  8859  mulle0r  8900  suprzclex  9350  peano5uzti  9360  supinfneg  9594  infsupneg  9595  qapne  9638  xrlelttr  9805  xrltletr  9806  xrre  9819  xaddge0  9877  xle2add  9878  xlt2add  9879  divelunit  10001  fzass4  10061  fzocatel  10198  exbtwnzlemex  10249  rebtwn2z  10254  qbtwnre  10256  modqid  10348  modqcyc  10358  modqaddabs  10361  modqaddmod  10362  mulqaddmodid  10363  modqadd2mod  10373  modqltm1p1mod  10375  modqsubmod  10381  modqsubmodmod  10382  modqmulmod  10388  modqmulmodr  10389  modqaddmulmod  10390  modqsubdir  10392  frec2uzisod  10406  iseqovex  10455  seqvalcd  10458  seqf  10460  seqovcd  10462  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  iseqf1olemnab  10487  seq3id2  10508  seq3distr  10512  expcl2lemap  10531  expnegzap  10553  ltexp2a  10571  le2sq2  10595  nn0ltexp2  10688  nn0opth2  10703  bcval5  10742  hashcl  10760  hashen  10763  fihashdom  10782  hashunlem  10783  hashun  10784  fimaxq  10806  zfz1isolem1  10819  zfz1iso  10820  cvg1nlemres  10993  cvg1n  10994  recvguniq  11003  resqrexlemp1rp  11014  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemex  11033  sqrtmul  11043  sqrtsq  11052  absexpzap  11088  absle  11097  abs3lem  11119  amgm2  11126  maxleastlt  11223  maxltsup  11226  fimaxre2  11234  xrmaxleastlt  11263  xrmaxltsup  11265  xrmaxaddlem  11267  climcn2  11316  addcn2  11317  mulcn2  11319  reccn2ap  11320  climcau  11354  summodclem2  11389  summodc  11390  fsumf1o  11397  fisumss  11399  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  fsum2dlemstep  11441  mptfzshft  11449  fsumrev  11450  fsummulc2  11455  modfsummod  11465  fsumrelem  11478  binom  11491  cvgratnn  11538  mertenslemub  11541  prodmodc  11585  zproddc  11586  fprodf1o  11595  fprodssdc  11597  fprodmul  11598  fprodrev  11626  fprod2dlemstep  11629  efcllem  11666  tanaddaplem  11745  dvdsval2  11796  moddvds  11805  dvdsabseq  11852  dvdsflip  11856  oexpneg  11881  fldivndvdslt  11939  zsupcllemstep  11945  zssinfcl  11948  suprzubdc  11952  zsupssdc  11954  suprzcl2dc  11955  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemeu  12007  dfgcd3  12010  bezout  12011  dvdsmulgcd  12025  bezoutr  12032  ialgrlem1st  12041  lcmgcdlem  12076  coprmdvds2  12092  qredeu  12096  rpdvds  12098  isprm5lem  12140  isprm6  12146  pw2dvdslemn  12164  nonsq  12206  crth  12223  eulerthlemh  12230  pclemdc  12287  pcprendvds2  12290  pceu  12294  pcval  12295  pczpre  12296  pcmul  12300  pcqmul  12302  pcqcl  12305  pcid  12322  pcneg  12323  pcgcd1  12326  pc2dvds  12328  pcprmpw2  12331  difsqpwdvds  12336  pcmpt  12340  pockthg  12354  1arith  12364  mul4sq  12391  ennnfonelemg  12403  ennnfonelemex  12414  ennnfonelemrnh  12416  ennnfonelemrn  12419  ennnfonelemdm  12420  ennnfonelemnn0  12422  ennnfonelemim  12424  ennnfone  12425  ctinfomlemom  12427  ctinf  12430  ctiunctlemfo  12439  nninfdclemcl  12448  nninfdclemf  12449  nninfdclemp1  12450  unbendc  12454  isstruct2r  12472  setscom  12501  qusval  12743  ercpbl  12749  opifismgmdc  12789  grprinvlem  12803  grpridd  12805  mndpropd  12840  issubmnd  12842  submnd0  12844  mhmf1o  12860  0mhm  12872  mhmco  12873  mhmima  12874  mhmeql  12875  grppropd  12892  grpinvid1  12923  grpinvid2  12924  grplcan  12931  grplmulf1o  12943  grpnpncan0  12965  dfgrp3mlem  12967  grplactcnv  12971  mulgval  12985  mulgfng  12986  mulg1  12989  mulgnnp1  12990  mulgneg  13000  mulgnndir  13010  mulgdirlem  13012  mulgnn0ass  13017  mulgass  13018  subgmulg  13046  issubg4m  13051  subgintm  13056  0nsg  13072  eqgcpbl  13085  ablpncan3  13118  srglmhm  13174  srgrmhm  13175  ringpropd  13215  dvdsrvald  13260  dvdsrd  13261  dvdsrex  13265  dvdsrtr  13268  unitgrp  13283  unitpropdg  13315  subrgintm  13362  aprap  13374  epttop  13560  topssnei  13632  restbasg  13638  restopnb  13651  cnfval  13664  cnpfval  13665  iscnp4  13688  cnpnei  13689  cnptopco  13692  cncnp  13700  cnrest2  13706  cnptoprest  13709  cnptoprest2  13710  lmss  13716  lmtopcnp  13720  neitx  13738  txcnp  13741  txrest  13746  txdis  13747  txlm  13749  cnmpt21  13761  imasnopn  13769  xmetres2  13849  blvalps  13858  blval  13859  bl2in  13873  blhalf  13878  blssps  13897  blss  13898  blssexps  13899  blssex  13900  ssblex  13901  blin2  13902  metss2lem  13967  bdmetval  13970  bdmopn  13974  metrest  13976  xmetxp  13977  xmetxpbl  13978  xmettx  13980  metcnp3  13981  txmetcnp  13988  addcncntoplem  14021  elcncf2  14031  mulc1cncf  14046  cncfco  14048  cncfmet  14049  mulcncf  14061  dedekindeulemub  14066  dedekindeulemloc  14067  dedekindeulemlu  14069  dedekindeu  14071  suplociccex  14073  dedekindicclemub  14075  dedekindicclemloc  14076  dedekindicclemlu  14078  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthdec  14092  limcimolemlt  14103  limcimo  14104  cnplimccntop  14109  limccnp2lem  14115  limccnp2cntop  14116  dvfvalap  14120  dveflem  14157  reeff1olem  14162  reeff1oleme  14163  eflt  14166  sin0pilem2  14173  pilem3  14174  ptolemy  14215  ioocosf1o  14245  cxplt  14306  cxple  14307  cxplt3  14310  apcxp2  14328  rprelogbmul  14343  rprelogbdiv  14345  logbgt0b  14354  logbgcd1irrap  14358  lgsdir2lem5  14403  lgsdir  14406  lgsdi  14408  lgsne0  14409  lgseisenlem2  14421  2sqlem6  14437  2sqlem10  14442  nnti  14714  pwtrufal  14717  pwf1oexmid  14719  sssneq  14721  qdencn  14745  cvgcmp2n  14751  trilpolemlt1  14759  trirec0  14762  trirec0xor  14763  redc0  14775  reap0  14776  nconstwlpolemgt0  14781  neap0mkv  14786  supfz  14788  inffz  14789