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  5252  fcof1  5733  fliftfun  5746  sbthlemi6  6906  sbthlemi8  6908  addcmpblnq  7287  mulcmpblnq  7288  ordpipqqs  7294  enq0tr  7354  addcmpblnq0  7363  mulcmpblnq0  7364  nnnq0lem1  7366  addnq0mo  7367  mulnq0mo  7368  prarloclemcalc  7422  addlocpr  7456  distrlem4prl  7504  distrlem4pru  7505  addcmpblnr  7659  mulcmpblnrlemg  7660  mulcmpblnr  7661  prsrlem1  7662  addsrmo  7663  mulsrmo  7664  ltsrprg  7667  apreap  8462  apreim  8478  divdivdivap  8586  divsubdivap  8601  ledivdiv  8761  lediv12a  8765  exbtwnz  10150  seq3caopr  10382  leexp2r  10473  zfz1iso  10712  recvguniq  10895  rsqrmo  10927  summodclem2  11279  prodmodclem2  11474  prodmodc  11475  qredeu  11974  pw2dvdseu  12043  epttop  12501  txdis1cn  12689  metequiv2  12907  cncfmptc  12993  cncfmptid  12994  addccncf  12997  negcncf  12999  dedekindicclemicc  13021