Theorem simprlr 538

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  imain  5341  fcof1  5833  fliftfun  5846  sbthlemi6  7037  sbthlemi8  7039  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  enq0tr  7520  addcmpblnq0  7529  mulcmpblnq0  7530  nnnq0lem1  7532  addnq0mo  7533  mulnq0mo  7534  prarloclemcalc  7588  addlocpr  7622  distrlem4prl  7670  distrlem4pru  7671  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  prsrlem1  7828  addsrmo  7829  mulsrmo  7830  ltsrprg  7833  apreap  8633  apreim  8649  aptap  8696  divdivdivap  8759  divsubdivap  8774  ledivdiv  8936  lediv12a  8940  exbtwnz  10359  seq3caopr  10606  seqcaoprg  10607  leexp2r  10704  zfz1iso  10952  recvguniq  11179  rsqrmo  11211  summodclem2  11566  prodmodclem2  11761  prodmodc  11762  qredeu  12292  pw2dvdseu  12363  pcadd  12536  mhmpropd  13170  grprcan  13241  isnsg3  13415  ghmpreima  13474  rngpropd  13589  ringpropd  13672  islmodd  13927  lmodprop2d  13982  lss1d  14017  epttop  14412  txdis1cn  14600  metequiv2  14818  cncfmptc  14918  cncfmptid  14919  addccncf  14922  negcncf  14927  dedekindicclemicc  14954  mpodvdsmulf1o  15312  2sqlem5  15446  2sqlem9  15451