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  5414  fcof1  5929  fliftfun  5942  sbthlemi6  7166  sbthlemi8  7168  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  enq0tr  7659  addcmpblnq0  7668  mulcmpblnq0  7669  nnnq0lem1  7671  addnq0mo  7672  mulnq0mo  7673  prarloclemcalc  7727  addlocpr  7761  distrlem4prl  7809  distrlem4pru  7810  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  prsrlem1  7967  addsrmo  7968  mulsrmo  7969  ltsrprg  7972  apreap  8772  apreim  8788  aptap  8835  divdivdivap  8898  divsubdivap  8913  ledivdiv  9075  lediv12a  9079  exbtwnz  10516  seq3caopr  10763  seqcaoprg  10764  leexp2r  10861  zfz1iso  11111  wrd2ind  11313  swrdccat  11325  recvguniq  11578  rsqrmo  11610  summodclem2  11966  prodmodclem2  12161  prodmodc  12162  qredeu  12692  pw2dvdseu  12763  pcadd  12936  mhmpropd  13572  grprcan  13643  isnsg3  13817  ghmpreima  13876  rngpropd  13992  ringpropd  14075  islmodd  14331  lmodprop2d  14386  lss1d  14421  epttop  14843  txdis1cn  15031  metequiv2  15249  cncfmptc  15349  cncfmptid  15350  addccncf  15353  negcncf  15358  dedekindicclemicc  15385  mpodvdsmulf1o  15743  2sqlem5  15877  2sqlem9  15882