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  5336  fcof1  5826  fliftfun  5839  sbthlemi6  7021  sbthlemi8  7023  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  enq0tr  7494  addcmpblnq0  7503  mulcmpblnq0  7504  nnnq0lem1  7506  addnq0mo  7507  mulnq0mo  7508  prarloclemcalc  7562  addlocpr  7596  distrlem4prl  7644  distrlem4pru  7645  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  prsrlem1  7802  addsrmo  7803  mulsrmo  7804  ltsrprg  7807  apreap  8606  apreim  8622  aptap  8669  divdivdivap  8732  divsubdivap  8747  ledivdiv  8909  lediv12a  8913  exbtwnz  10319  seq3caopr  10566  seqcaoprg  10567  leexp2r  10664  zfz1iso  10912  recvguniq  11139  rsqrmo  11171  summodclem2  11525  prodmodclem2  11720  prodmodc  11721  qredeu  12235  pw2dvdseu  12306  pcadd  12478  mhmpropd  13038  grprcan  13109  isnsg3  13277  ghmpreima  13336  rngpropd  13451  ringpropd  13534  islmodd  13789  lmodprop2d  13844  lss1d  13879  epttop  14258  txdis1cn  14446  metequiv2  14664  cncfmptc  14750  cncfmptid  14751  addccncf  14754  negcncf  14759  dedekindicclemicc  14786  2sqlem5  15206  2sqlem9  15211