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  5437  fcof1  5955  fliftfun  5968  sbthlemi6  7231  sbthlemi8  7233  suppeqfsuppbi  7247  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  enq0tr  7745  addcmpblnq0  7754  mulcmpblnq0  7755  nnnq0lem1  7757  addnq0mo  7758  mulnq0mo  7759  prarloclemcalc  7813  addlocpr  7847  distrlem4prl  7895  distrlem4pru  7896  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  prsrlem1  8053  addsrmo  8054  mulsrmo  8055  ltsrprg  8058  apreap  8857  apreim  8873  aptap  8920  divdivdivap  8983  divsubdivap  8998  ledivdiv  9160  lediv12a  9164  exbtwnz  10606  seq3caopr  10853  seqcaoprg  10854  leexp2r  10951  hashfibclem  11199  zfz1iso  11206  wrd2ind  11408  swrdccat  11420  recvguniq  11673  rsqrmo  11705  summodclem2  12061  prodmodclem2  12256  prodmodc  12257  qredeu  12787  pw2dvdseu  12858  pcadd  13031  mhmpropd  13668  grprcan  13739  isnsg3  13913  ghmpreima  13972  rngpropd  14088  ringpropd  14171  islmodd  14428  lmodprop2d  14483  lss1d  14518  epttop  14942  txdis1cn  15130  metequiv2  15348  cncfmptc  15448  cncfmptid  15449  addccncf  15452  negcncf  15457  dedekindicclemicc  15484  mpodvdsmulf1o  15845  2sqlem5  15979  2sqlem9  15984