Theorem simprl 503

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rl  1027  simp2rl  1031  simp3rl  1035  rmob  2967  disjiun  3888  reg3exmidlemwe  4451  0xp  4577  imainss  4910  fvmptt  5464  fcof1o  5642  isotr  5669  riota5f  5706  ovmpodf  5854  grprinvlem  5917  grpridd  5919  unielxp  6024  fnmpoovd  6064  1stconst  6070  2ndconst  6071  cnvf1olem  6073  tfrlemi14d  6182  tfrexlem  6183  tfr1onlemres  6198  tfrcllemres  6211  tfrcldm  6212  frecabcl  6248  nnaordi  6356  swoer  6409  qliftfun  6463  ecopovsymg  6480  th3qlem1  6483  mapen  6691  mapxpen  6693  fidifsnen  6715  fisbth  6728  findcard2d  6736  findcard2sd  6737  diffisn  6738  diffifi  6739  ac6sfi  6743  fimax2gtri  6746  fientri3  6754  nnwetri  6755  unsnfi  6758  unsnfidcex  6759  unsnfidcel  6760  fisseneq  6771  fidcenumlemrk  6792  fidcenumlemr  6793  isbth  6805  ordiso2  6870  difinfsnlem  6934  difinfinf  6936  ctmlemr  6943  ctssdccl  6946  fodjum  6966  fodju0  6967  exmidfodomrlemrALT  7004  dfplpq2  7104  dfmpq2  7105  mulpipqqs  7123  distrnqg  7137  ltexnqq  7158  subhalfnqq  7164  distrnq0  7209  prarloclemup  7245  prarloclem3  7247  prarloc  7253  genplt2i  7260  nqprl  7301  nqpru  7302  prmuloc  7316  mullocpr  7321  distrlem4prl  7334  distrlem4pru  7335  ltaddpr  7347  ltexprlemopl  7351  ltexprlemlol  7352  ltexprlemopu  7353  ltexprlemupu  7354  ltexprlemrl  7360  ltexprlemru  7362  addcanprleml  7364  addcanprlemu  7365  ltaprlem  7368  ltaprg  7369  prplnqu  7370  addextpr  7371  recexprlemdisj  7380  recexprlemloc  7381  recexprlem1ssl  7383  aptiprleml  7389  aptiprlemu  7390  ltmprr  7392  archpr  7393  cauappcvgprlemopl  7396  cauappcvgprlemopu  7398  cauappcvgprlemdisj  7401  cauappcvgprlemloc  7402  cauappcvgprlem1  7409  cauappcvgprlem2  7410  cauappcvgprlemlim  7411  caucvgprlemnkj  7416  caucvgprlemopl  7419  caucvgprlemopu  7421  caucvgprlemdisj  7424  caucvgprlemloc  7425  caucvgprlem2  7430  caucvgprprlemnkltj  7439  caucvgprprlemnkeqj  7440  caucvgprprlemnjltk  7441  caucvgprprlemmu  7445  caucvgprprlemopl  7447  caucvgprprlemopu  7449  caucvgprprlemdisj  7452  caucvgprprlemloc  7453  caucvgprprlemexbt  7456  caucvgprprlemaddq  7458  caucvgprprlem2  7460  recexgt0sr  7510  mulgt0sr  7514  prsrriota  7524  caucvgsrlemoffres  7536  cnm  7561  addcnsr  7563  mulcnsr  7564  mulcnsrec  7572  axaddcl  7593  axmulcl  7595  axmulcom  7600  rereceu  7618  recriota  7619  axcaucvglemres  7628  lelttr  7769  ltletr  7770  readdcan  7819  addcan  7859  addcan2  7860  addsub4  7922  ltadd2  8094  le2add  8119  lt2add  8120  lt2sub  8135  le2sub  8136  eqord1  8158  rimul  8259  rereim  8260  ltmul1  8266  apreim  8277  mulreim  8278  apcotr  8281  apadd1  8282  addext  8284  apneg  8285  mulext1  8286  mulext  8288  ltleap  8305  mulap0  8322  mulcanapd  8329  receuap  8337  rec11ap  8377  rec11rap  8378  divdivdivap  8380  ddcanap  8393  divadddivap  8394  conjmulap  8396  prodgt0gt0  8513  prodge0  8516  ltmul12a  8522  lemulge11  8528  lt2mul2div  8541  ltrec  8545  lerec  8546  lt2msq  8548  lerec2  8551  le2msq  8563  msq11  8564  ledivp1  8565  mulle0r  8606  suprzclex  9047  peano5uzti  9057  supinfneg  9286  infsupneg  9287  qapne  9327  xrlelttr  9476  xrltletr  9477  xrre  9490  xaddge0  9548  xle2add  9549  xlt2add  9550  divelunit  9672  fzass4  9729  fzocatel  9863  exbtwnzlemex  9914  rebtwn2z  9919  qbtwnre  9921  modqid  10009  modqcyc  10019  modqaddabs  10022  modqaddmod  10023  mulqaddmodid  10024  modqadd2mod  10034  modqltm1p1mod  10036  modqsubmod  10042  modqsubmodmod  10043  modqmulmod  10049  modqmulmodr  10050  modqaddmulmod  10051  modqsubdir  10053  frec2uzisod  10067  iseqovex  10116  seqvalcd  10119  seqf  10121  seqovcd  10123  seq3fveq2  10129  seq3shft2  10133  monoord  10136  seq3split  10139  iseqf1olemnab  10148  seq3id2  10169  seq3distr  10173  expcl2lemap  10192  expnegzap  10214  ltexp2a  10232  le2sq2  10255  nn0opth2  10357  bcval5  10396  hashcl  10414  hashen  10417  fihashdom  10436  hashunlem  10437  hashun  10438  fimaxq  10460  zfz1isolem1  10470  zfz1iso  10471  cvg1nlemres  10643  cvg1n  10644  recvguniq  10653  resqrexlemp1rp  10664  resqrexlemoverl  10679  resqrexlemglsq  10680  resqrexlemex  10683  sqrtmul  10693  sqrtsq  10702  absexpzap  10738  absle  10747  abs3lem  10769  amgm2  10776  maxleastlt  10873  maxltsup  10876  fimaxre2  10884  xrmaxleastlt  10911  xrmaxltsup  10913  xrmaxaddlem  10915  climcn2  10964  addcn2  10965  mulcn2  10967  reccn2ap  10968  climcau  11002  summodclem2  11037  summodc  11038  fsumf1o  11045  fisumss  11047  fsum3cvg3  11051  fsumcl2lem  11053  fsumadd  11061  fsum2dlemstep  11089  mptfzshft  11097  fsumrev  11098  fsummulc2  11103  modfsummod  11113  fsumrelem  11126  binom  11139  cvgratnn  11186  mertenslemub  11189  efcllem  11210  tanaddaplem  11290  dvdsval2  11338  moddvds  11344  dvdsabseq  11387  dvdsflip  11391  oexpneg  11416  fldivndvdslt  11474  zsupcllemstep  11480  zssinfcl  11483  bezoutlemnewy  11524  bezoutlemstep  11525  bezoutlemeu  11535  dfgcd3  11538  bezout  11539  dvdsmulgcd  11553  bezoutr  11560  ialgrlem1st  11563  lcmgcdlem  11598  coprmdvds2  11614  qredeu  11618  rpdvds  11620  isprm6  11665  pw2dvdslemn  11682  nonsq  11724  crth  11739  ennnfonelemg  11755  ennnfonelemex  11766  ennnfonelemrnh  11768  ennnfonelemrn  11771  ennnfonelemdm  11772  ennnfonelemnn0  11774  ennnfonelemim  11776  ennnfone  11777  ctinfomlemom  11779  ctinf  11782  ctiunctlemfo  11789  isstruct2r  11807  setscom  11836  epttop  12096  topssnei  12168  restbasg  12174  restopnb  12187  cnfval  12200  cnpfval  12201  iscnp4  12223  cnpnei  12224  cnptopco  12227  cncnp  12235  cnrest2  12241  cnptoprest  12244  cnptoprest2  12245  lmss  12251  lmtopcnp  12255  neitx  12273  txcnp  12276  txrest  12281  txdis  12282  txlm  12284  cnmpt21  12296  imasnopn  12304  xmetres2  12362  blvalps  12371  blval  12372  bl2in  12386  blhalf  12391  blssps  12410  blss  12411  blssexps  12412  blssex  12413  ssblex  12414  blin2  12415  metss2lem  12480  bdmetval  12483  bdmopn  12487  metrest  12489  xmetxp  12490  xmetxpbl  12491  xmettx  12493  metcnp3  12494  txmetcnp  12501  addcncntoplem  12531  elcncf2  12541  mulc1cncf  12556  cncfco  12558  cncfmet  12559  mulcncf  12571  limcimolemlt  12583  limcimo  12584  cnplimccntop  12589  limccnp2lem  12595  limccnp2cntop  12596  dvfvalap  12599  nnti  12874  pwtrufal  12875  pwf1oexmid  12877  qdencn  12903  cvgcmp2n  12909  trilpolemlt1  12915  supfz  12918  inffz  12919