Theorem simprlr 544

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 494	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  imain  5463  fcof1  5989  fliftfun  6002  sbthlemi6  7279  sbthlemi8  7281  suppeqfsuppbi  7295  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  enq0tr  7801  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  addnq0mo  7814  mulnq0mo  7815  prarloclemcalc  7869  addlocpr  7903  distrlem4prl  7951  distrlem4pru  7952  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  addsrmo  8110  mulsrmo  8111  ltsrprg  8114  apreap  8916  apreim  8932  aptap  8979  divdivdivap  9044  divsubdivap  9059  ledivdiv  9221  lediv12a  9225  exbtwnz  10687  seq3caopr  10934  seqcaoprg  10935  leexp2r  11032  hashfibclem  11284  hashf1lem1  11287  hashf1lem2  11288  zfz1iso  11295  wrd2ind  11497  swrdccat  11509  recvguniq  11763  rsqrmo  11795  summodclem2  12151  prodmodclem2  12346  prodmodc  12347  qredeu  12877  pw2dvdseu  12948  pcadd  13121  ballotfilemfc0  13234  ballotfilemfcc  13235  mhmpropd  13775  grprcan  13844  isnsg3  14012  ghmpreima  14071  rngpropd  14256  ringpropd  14345  islmodd  14631  lmodprop2d  14687  lss1d  14722  assamulgscmlem2  15044  epttop  15193  txdis1cn  15381  metequiv2  15599  cncfmptc  15699  cncfmptid  15700  addccncf  15703  negcncf  15708  dedekindicclemicc  15735  mpodvdsmulf1o  16110  2sqlem5  16250  2sqlem9  16255