Theorem simprlr 527

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 481	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  5200  fcof1  5677  fliftfun  5690  sbthlemi6  6843  sbthlemi8  6845  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  enq0tr  7235  addcmpblnq0  7244  mulcmpblnq0  7245  nnnq0lem1  7247  addnq0mo  7248  mulnq0mo  7249  prarloclemcalc  7303  addlocpr  7337  distrlem4prl  7385  distrlem4pru  7386  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  prsrlem1  7543  addsrmo  7544  mulsrmo  7545  ltsrprg  7548  apreap  8342  apreim  8358  divdivdivap  8466  divsubdivap  8481  ledivdiv  8641  lediv12a  8645  exbtwnz  10021  seq3caopr  10249  leexp2r  10340  zfz1iso  10577  recvguniq  10760  rsqrmo  10792  summodclem2  11144  qredeu  11767  pw2dvdseu  11835  epttop  12248  txdis1cn  12436  metequiv2  12654  cncfmptc  12740  cncfmptid  12741  addccncf  12744  negcncf  12746  dedekindicclemicc  12768