Theorem simprlr 528

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 482	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  5270  fcof1  5751  fliftfun  5764  sbthlemi6  6927  sbthlemi8  6929  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  enq0tr  7375  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  addnq0mo  7388  mulnq0mo  7389  prarloclemcalc  7443  addlocpr  7477  distrlem4prl  7525  distrlem4pru  7526  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  prsrlem1  7683  addsrmo  7684  mulsrmo  7685  ltsrprg  7688  apreap  8485  apreim  8501  divdivdivap  8609  divsubdivap  8624  ledivdiv  8785  lediv12a  8789  exbtwnz  10186  seq3caopr  10418  leexp2r  10509  zfz1iso  10754  recvguniq  10937  rsqrmo  10969  summodclem2  11323  prodmodclem2  11518  prodmodc  11519  qredeu  12029  pw2dvdseu  12100  pcadd  12271  epttop  12740  txdis1cn  12928  metequiv2  13146  cncfmptc  13232  cncfmptid  13233  addccncf  13236  negcncf  13238  dedekindicclemicc  13260  2sqlem5  13605  2sqlem9  13610