Theorem simprlr 533

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 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 487	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  imain  5280  fcof1  5762  fliftfun  5775  sbthlemi6  6939  sbthlemi8  6941  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  enq0tr  7396  addcmpblnq0  7405  mulcmpblnq0  7406  nnnq0lem1  7408  addnq0mo  7409  mulnq0mo  7410  prarloclemcalc  7464  addlocpr  7498  distrlem4prl  7546  distrlem4pru  7547  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  prsrlem1  7704  addsrmo  7705  mulsrmo  7706  ltsrprg  7709  apreap  8506  apreim  8522  divdivdivap  8630  divsubdivap  8645  ledivdiv  8806  lediv12a  8810  exbtwnz  10207  seq3caopr  10439  leexp2r  10530  zfz1iso  10776  recvguniq  10959  rsqrmo  10991  summodclem2  11345  prodmodclem2  11540  prodmodc  11541  qredeu  12051  pw2dvdseu  12122  pcadd  12293  mhmpropd  12689  grprcan  12740  epttop  12884  txdis1cn  13072  metequiv2  13290  cncfmptc  13376  cncfmptid  13377  addccncf  13380  negcncf  13382  dedekindicclemicc  13404  2sqlem5  13749  2sqlem9  13754