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  5341  fcof1  5833  fliftfun  5846  sbthlemi6  7037  sbthlemi8  7039  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  enq0tr  7518  addcmpblnq0  7527  mulcmpblnq0  7528  nnnq0lem1  7530  addnq0mo  7531  mulnq0mo  7532  prarloclemcalc  7586  addlocpr  7620  distrlem4prl  7668  distrlem4pru  7669  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  prsrlem1  7826  addsrmo  7827  mulsrmo  7828  ltsrprg  7831  apreap  8631  apreim  8647  aptap  8694  divdivdivap  8757  divsubdivap  8772  ledivdiv  8934  lediv12a  8938  exbtwnz  10357  seq3caopr  10604  seqcaoprg  10605  leexp2r  10702  zfz1iso  10950  recvguniq  11177  rsqrmo  11209  summodclem2  11564  prodmodclem2  11759  prodmodc  11760  qredeu  12290  pw2dvdseu  12361  pcadd  12534  mhmpropd  13168  grprcan  13239  isnsg3  13413  ghmpreima  13472  rngpropd  13587  ringpropd  13670  islmodd  13925  lmodprop2d  13980  lss1d  14015  epttop  14410  txdis1cn  14598  metequiv2  14816  cncfmptc  14916  cncfmptid  14917  addccncf  14920  negcncf  14925  dedekindicclemicc  14952  mpodvdsmulf1o  15310  2sqlem5  15444  2sqlem9  15449