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  5379  fcof1  5880  fliftfun  5893  sbthlemi6  7097  sbthlemi8  7099  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  enq0tr  7589  addcmpblnq0  7598  mulcmpblnq0  7599  nnnq0lem1  7601  addnq0mo  7602  mulnq0mo  7603  prarloclemcalc  7657  addlocpr  7691  distrlem4prl  7739  distrlem4pru  7740  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  prsrlem1  7897  addsrmo  7898  mulsrmo  7899  ltsrprg  7902  apreap  8702  apreim  8718  aptap  8765  divdivdivap  8828  divsubdivap  8843  ledivdiv  9005  lediv12a  9009  exbtwnz  10437  seq3caopr  10684  seqcaoprg  10685  leexp2r  10782  zfz1iso  11030  wrd2ind  11221  swrdccat  11233  recvguniq  11472  rsqrmo  11504  summodclem2  11859  prodmodclem2  12054  prodmodc  12055  qredeu  12585  pw2dvdseu  12656  pcadd  12829  mhmpropd  13465  grprcan  13536  isnsg3  13710  ghmpreima  13769  rngpropd  13884  ringpropd  13967  islmodd  14222  lmodprop2d  14277  lss1d  14312  epttop  14729  txdis1cn  14917  metequiv2  15135  cncfmptc  15235  cncfmptid  15236  addccncf  15239  negcncf  15244  dedekindicclemicc  15271  mpodvdsmulf1o  15629  2sqlem5  15763  2sqlem9  15768