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

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  5461  fcof1  5983  fliftfun  5996  sbthlemi6  7273  sbthlemi8  7275  suppeqfsuppbi  7289  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  enq0tr  7795  addcmpblnq0  7804  mulcmpblnq0  7805  nnnq0lem1  7807  addnq0mo  7808  mulnq0mo  7809  prarloclemcalc  7863  addlocpr  7897  distrlem4prl  7945  distrlem4pru  7946  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  prsrlem1  8103  addsrmo  8104  mulsrmo  8105  ltsrprg  8108  apreap  8909  apreim  8925  aptap  8972  divdivdivap  9037  divsubdivap  9052  ledivdiv  9214  lediv12a  9218  exbtwnz  10668  seq3caopr  10915  seqcaoprg  10916  leexp2r  11013  hashfibclem  11265  hashf1lem1  11268  hashf1lem2  11269  zfz1iso  11276  wrd2ind  11478  swrdccat  11490  recvguniq  11744  rsqrmo  11776  summodclem2  12132  prodmodclem2  12327  prodmodc  12328  qredeu  12858  pw2dvdseu  12929  pcadd  13102  ballotfilemfc0  13215  ballotfilemfcc  13216  mhmpropd  13756  grprcan  13825  isnsg3  13993  ghmpreima  14052  rngpropd  14237  ringpropd  14326  islmodd  14612  lmodprop2d  14668  lss1d  14703  assamulgscmlem2  15025  epttop  15174  txdis1cn  15362  metequiv2  15580  cncfmptc  15680  cncfmptid  15681  addccncf  15684  negcncf  15689  dedekindicclemicc  15716  mpodvdsmulf1o  16087  2sqlem5  16221  2sqlem9  16226