Theorem simprlr 538

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  5340  fcof1  5830  fliftfun  5843  sbthlemi6  7028  sbthlemi8  7030  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  enq0tr  7501  addcmpblnq0  7510  mulcmpblnq0  7511  nnnq0lem1  7513  addnq0mo  7514  mulnq0mo  7515  prarloclemcalc  7569  addlocpr  7603  distrlem4prl  7651  distrlem4pru  7652  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  prsrlem1  7809  addsrmo  7810  mulsrmo  7811  ltsrprg  7814  apreap  8614  apreim  8630  aptap  8677  divdivdivap  8740  divsubdivap  8755  ledivdiv  8917  lediv12a  8921  exbtwnz  10340  seq3caopr  10587  seqcaoprg  10588  leexp2r  10685  zfz1iso  10933  recvguniq  11160  rsqrmo  11192  summodclem2  11547  prodmodclem2  11742  prodmodc  11743  qredeu  12265  pw2dvdseu  12336  pcadd  12509  mhmpropd  13098  grprcan  13169  isnsg3  13337  ghmpreima  13396  rngpropd  13511  ringpropd  13594  islmodd  13849  lmodprop2d  13904  lss1d  13939  epttop  14326  txdis1cn  14514  metequiv2  14732  cncfmptc  14832  cncfmptid  14833  addccncf  14836  negcncf  14841  dedekindicclemicc  14868  mpodvdsmulf1o  15226  2sqlem5  15360  2sqlem9  15365