Theorem simprlr 540

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprlr	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 110	. 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:  imain  5443  fcof1  5962  fliftfun  5975  sbthlemi6  7245  sbthlemi8  7247  suppeqfsuppbi  7261  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  addnq0mo  7778  mulnq0mo  7779  prarloclemcalc  7833  addlocpr  7867  distrlem4prl  7915  distrlem4pru  7916  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  addsrmo  8074  mulsrmo  8075  ltsrprg  8078  apreap  8879  apreim  8895  aptap  8942  divdivdivap  9007  divsubdivap  9022  ledivdiv  9184  lediv12a  9188  exbtwnz  10637  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  hashfibclem  11234  zfz1iso  11241  wrd2ind  11443  swrdccat  11455  recvguniq  11708  rsqrmo  11740  summodclem2  12096  prodmodclem2  12291  prodmodc  12292  qredeu  12822  pw2dvdseu  12893  pcadd  13066  ballotfilemfc0  13179  ballotfilemfcc  13180  mhmpropd  13724  grprcan  13795  isnsg3  13963  ghmpreima  14022  rngpropd  14197  ringpropd  14284  islmodd  14570  lmodprop2d  14625  lss1d  14660  epttop  15084  txdis1cn  15272  metequiv2  15490  cncfmptc  15590  cncfmptid  15591  addccncf  15594  negcncf  15599  dedekindicclemicc  15626  mpodvdsmulf1o  15987  2sqlem5  16121  2sqlem9  16126