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  5409  fcof1  5919  fliftfun  5932  sbthlemi6  7155  sbthlemi8  7157  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  enq0tr  7647  addcmpblnq0  7656  mulcmpblnq0  7657  nnnq0lem1  7659  addnq0mo  7660  mulnq0mo  7661  prarloclemcalc  7715  addlocpr  7749  distrlem4prl  7797  distrlem4pru  7798  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  prsrlem1  7955  addsrmo  7956  mulsrmo  7957  ltsrprg  7960  apreap  8760  apreim  8776  aptap  8823  divdivdivap  8886  divsubdivap  8901  ledivdiv  9063  lediv12a  9067  exbtwnz  10503  seq3caopr  10750  seqcaoprg  10751  leexp2r  10848  zfz1iso  11098  wrd2ind  11297  swrdccat  11309  recvguniq  11549  rsqrmo  11581  summodclem2  11936  prodmodclem2  12131  prodmodc  12132  qredeu  12662  pw2dvdseu  12733  pcadd  12906  mhmpropd  13542  grprcan  13613  isnsg3  13787  ghmpreima  13846  rngpropd  13961  ringpropd  14044  islmodd  14300  lmodprop2d  14355  lss1d  14390  epttop  14807  txdis1cn  14995  metequiv2  15213  cncfmptc  15313  cncfmptid  15314  addccncf  15317  negcncf  15322  dedekindicclemicc  15349  mpodvdsmulf1o  15707  2sqlem5  15841  2sqlem9  15846