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  5213  fcof1  5692  fliftfun  5705  sbthlemi6  6858  sbthlemi8  6860  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  enq0tr  7266  addcmpblnq0  7275  mulcmpblnq0  7276  nnnq0lem1  7278  addnq0mo  7279  mulnq0mo  7280  prarloclemcalc  7334  addlocpr  7368  distrlem4prl  7416  distrlem4pru  7417  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  prsrlem1  7574  addsrmo  7575  mulsrmo  7576  ltsrprg  7579  apreap  8373  apreim  8389  divdivdivap  8497  divsubdivap  8512  ledivdiv  8672  lediv12a  8676  exbtwnz  10059  seq3caopr  10287  leexp2r  10378  zfz1iso  10616  recvguniq  10799  rsqrmo  10831  summodclem2  11183  prodmodclem2  11378  prodmodc  11379  qredeu  11814  pw2dvdseu  11882  epttop  12298  txdis1cn  12486  metequiv2  12704  cncfmptc  12790  cncfmptid  12791  addccncf  12794  negcncf  12796  dedekindicclemicc  12818