Theorem simprl 497

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  simp1rl  1003  simp2rl  1007  simp3rl  1011  rmob  2906  reg3exmidlemwe  4321  0xp  4438  imainss  4759  fvmptt  5283  fcof1o  5449  isotr  5476  riota5f  5512  ovmpt2df  5652  grprinvlem  5715  grpridd  5717  unielxp  5820  1stconst  5862  2ndconst  5863  cnvf1olem  5865  tfrlemi14d  5970  tfrexlem  5971  nnaordi  6104  swoer  6157  qliftfun  6211  ecopovsymg  6228  th3qlem1  6231  fidifsnen  6355  fisbth  6367  findcard2d  6375  findcard2sd  6376  diffisn  6377  diffifi  6378  ac6sfi  6379  fientri3  6381  nnwetri  6382  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  ordiso2  6446  dfplpq2  6544  dfmpq2  6545  mulpipqqs  6563  distrnqg  6577  ltexnqq  6598  subhalfnqq  6604  distrnq0  6649  prarloclemup  6685  prarloclem3  6687  prarloc  6693  genplt2i  6700  nqprl  6741  nqpru  6742  prmuloc  6756  mullocpr  6761  distrlem4prl  6774  distrlem4pru  6775  ltaddpr  6787  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltaprlem  6808  ltaprg  6809  prplnqu  6810  addextpr  6811  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  archpr  6833  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgprlemlim  6851  caucvgprlemnkj  6856  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlem2  6870  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  caucvgprprlem2  6900  recexgt0sr  6950  mulgt0sr  6954  prsrriota  6964  caucvgsrlemoffres  6976  addcnsr  7002  mulcnsr  7003  mulcnsrec  7011  axaddcl  7032  axmulcl  7034  axmulcom  7037  rereceu  7055  recriota  7056  axcaucvglemres  7065  lelttr  7199  ltletr  7200  readdcan  7248  addcan  7288  addcan2  7289  addsub4  7351  ltadd2  7523  le2add  7548  lt2add  7549  lt2sub  7564  le2sub  7565  rimul  7685  rereim  7686  ltmul1  7692  apreim  7703  mulreim  7704  apcotr  7707  apadd1  7708  addext  7710  apneg  7711  mulext1  7712  mulext  7714  ltleap  7730  mulap0  7744  mulcanapd  7751  receuap  7759  rec11ap  7798  rec11rap  7799  divdivdivap  7801  ddcanap  7814  divadddivap  7815  conjmulap  7817  prodgt0gt0  7929  prodge0  7932  ltmul12a  7938  lemulge11  7944  lt2mul2div  7957  ltrec  7961  lerec  7962  lt2msq  7964  lerec2  7967  le2msq  7979  msq11  7980  ledivp1  7981  mulle0r  8022  suprzclex  8445  peano5uzti  8455  supinfneg  8683  infsupneg  8684  qapne  8724  xrlelttr  8876  xrltletr  8877  xrre  8887  divelunit  9024  fzass4  9080  fzocatel  9208  qbtwnzlemex  9259  rebtwn2z  9263  qbtwnre  9265  modqid  9351  modqcyc  9361  modqaddabs  9364  modqaddmod  9365  mulqaddmodid  9366  modqadd2mod  9376  modqltm1p1mod  9378  modqsubmod  9384  modqsubmodmod  9385  modqmulmod  9391  modqmulmodr  9392  modqaddmulmod  9393  modqsubdir  9395  frec2uzisod  9409  iseqovex  9439  iseqval  9440  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqdistr  9470  expivallem  9477  expcl2lemap  9488  expnegzap  9510  ltexp2a  9528  le2sq2  9551  nn0opth2  9651  ibcval5  9690  cvg1nlemres  9871  cvg1n  9872  recvguniq  9881  resqrexlemp1rp  9892  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemex  9911  sqrtmul  9921  sqrtsq  9930  absexpzap  9966  absle  9975  abs3lem  9997  amgm2  10004  maxleastlt  10101  maxltsup  10104  fimaxre2  10109  climcn2  10148  addcn2  10149  mulcn2  10151  climcau  10184  dvdsval2  10198  moddvds  10204  dvdsabseq  10247  dvdsflip  10251  oexpneg  10276  fldivndvdslt  10335  zsupcllemstep  10341  zssinfcl  10344  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemeu  10396  dfgcd3  10399  bezout  10400  dvdsmulgcd  10414  bezoutr  10421  ialgrlem1st  10424  lcmgcdlem  10459  coprmdvds2  10475  qredeu  10479  rpdvds  10481  isprm6  10526  pw2dvdslemn  10543  qdencn  10785