Theorem simprl 498

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 474	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  1006  simp2rl  1010  simp3rl  1014  rmob  2920  reg3exmidlemwe  4367  0xp  4486  imainss  4813  fvmptt  5357  fcof1o  5529  isotr  5556  riota5f  5593  ovmpt2df  5733  grprinvlem  5796  grpridd  5798  unielxp  5901  1stconst  5943  2ndconst  5944  cnvf1olem  5946  tfrlemi14d  6052  tfrexlem  6053  tfr1onlemres  6068  tfrcllemres  6081  tfrcldm  6082  frecabcl  6118  nnaordi  6219  swoer  6272  qliftfun  6326  ecopovsymg  6343  th3qlem1  6346  mapen  6514  mapxpen  6516  fidifsnen  6538  fisbth  6551  findcard2d  6559  findcard2sd  6560  diffisn  6561  diffifi  6562  ac6sfi  6566  fimax2gtri  6569  fientri3  6577  nnwetri  6578  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  fisseneq  6592  isbth  6620  ordiso2  6672  fodjuomnilemm  6745  fodjuomnilem0  6746  exmidfodomrlemrALT  6773  dfplpq2  6857  dfmpq2  6858  mulpipqqs  6876  distrnqg  6890  ltexnqq  6911  subhalfnqq  6917  distrnq0  6962  prarloclemup  6998  prarloclem3  7000  prarloc  7006  genplt2i  7013  nqprl  7054  nqpru  7055  prmuloc  7069  mullocpr  7074  distrlem4prl  7087  distrlem4pru  7088  ltaddpr  7100  ltexprlemopl  7104  ltexprlemlol  7105  ltexprlemopu  7106  ltexprlemupu  7107  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  ltaprlem  7121  ltaprg  7122  prplnqu  7123  addextpr  7124  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  aptiprleml  7142  aptiprlemu  7143  ltmprr  7145  archpr  7146  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlem1  7162  cauappcvgprlem2  7163  cauappcvgprlemlim  7164  caucvgprlemnkj  7169  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlem2  7183  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  caucvgprprlem2  7213  recexgt0sr  7263  mulgt0sr  7267  prsrriota  7277  caucvgsrlemoffres  7289  addcnsr  7315  mulcnsr  7316  mulcnsrec  7324  axaddcl  7345  axmulcl  7347  axmulcom  7350  rereceu  7368  recriota  7369  axcaucvglemres  7378  lelttr  7517  ltletr  7518  readdcan  7566  addcan  7606  addcan2  7607  addsub4  7669  ltadd2  7841  le2add  7866  lt2add  7867  lt2sub  7882  le2sub  7883  rimul  8003  rereim  8004  ltmul1  8010  apreim  8021  mulreim  8022  apcotr  8025  apadd1  8026  addext  8028  apneg  8029  mulext1  8030  mulext  8032  ltleap  8048  mulap0  8062  mulcanapd  8069  receuap  8077  rec11ap  8116  rec11rap  8117  divdivdivap  8119  ddcanap  8132  divadddivap  8133  conjmulap  8135  prodgt0gt0  8247  prodge0  8250  ltmul12a  8256  lemulge11  8262  lt2mul2div  8275  ltrec  8279  lerec  8280  lt2msq  8282  lerec2  8285  le2msq  8297  msq11  8298  ledivp1  8299  mulle0r  8340  suprzclex  8777  peano5uzti  8787  supinfneg  9015  infsupneg  9016  qapne  9056  xrlelttr  9203  xrltletr  9204  xrre  9214  divelunit  9351  fzass4  9407  fzocatel  9538  exbtwnzlemex  9589  rebtwn2z  9594  qbtwnre  9596  modqid  9684  modqcyc  9694  modqaddabs  9697  modqaddmod  9698  mulqaddmodid  9699  modqadd2mod  9709  modqltm1p1mod  9711  modqsubmod  9717  modqsubmodmod  9718  modqmulmod  9724  modqmulmodr  9725  modqaddmulmod  9726  modqsubdir  9728  frec2uzisod  9742  iseqovex  9787  iseqval  9788  iseqfclt  9794  iseqfveq2  9802  iseqshft2  9806  monoord  9809  iseqsplit  9812  iseqf1olemnab  9821  iseqid2  9843  iseqdistr  9846  expivallem  9854  expcl2lemap  9865  expnegzap  9887  ltexp2a  9905  le2sq2  9928  nn0opth2  10028  ibcval5  10067  hashcl  10085  hashen  10088  fihashdom  10107  hashunlem  10108  hashun  10109  fimaxq  10131  zfz1isolem1  10141  zfz1iso  10142  cvg1nlemres  10313  cvg1n  10314  recvguniq  10323  resqrexlemp1rp  10334  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemex  10353  sqrtmul  10363  sqrtsq  10372  absexpzap  10408  absle  10417  abs3lem  10439  amgm2  10446  maxleastlt  10543  maxltsup  10546  fimaxre2  10551  climcn2  10590  addcn2  10591  mulcn2  10593  climcau  10626  isummolem2  10661  isummo  10662  fsumf1o  10668  fisumss  10670  dvdsval2  10674  moddvds  10680  dvdsabseq  10723  dvdsflip  10727  oexpneg  10752  fldivndvdslt  10810  zsupcllemstep  10816  zssinfcl  10819  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlemeu  10871  dfgcd3  10874  bezout  10875  dvdsmulgcd  10889  bezoutr  10896  ialgrlem1st  10899  lcmgcdlem  10934  coprmdvds2  10950  qredeu  10954  rpdvds  10956  isprm6  11001  pw2dvdslemn  11018  nonsq  11060  crth  11075  nnti  11330  qdencn  11353