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  5361  fcof1  5859  fliftfun  5872  sbthlemi6  7071  sbthlemi8  7073  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  enq0tr  7554  addcmpblnq0  7563  mulcmpblnq0  7564  nnnq0lem1  7566  addnq0mo  7567  mulnq0mo  7568  prarloclemcalc  7622  addlocpr  7656  distrlem4prl  7704  distrlem4pru  7705  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  prsrlem1  7862  addsrmo  7863  mulsrmo  7864  ltsrprg  7867  apreap  8667  apreim  8683  aptap  8730  divdivdivap  8793  divsubdivap  8808  ledivdiv  8970  lediv12a  8974  exbtwnz  10400  seq3caopr  10647  seqcaoprg  10648  leexp2r  10745  zfz1iso  10993  recvguniq  11350  rsqrmo  11382  summodclem2  11737  prodmodclem2  11932  prodmodc  11933  qredeu  12463  pw2dvdseu  12534  pcadd  12707  mhmpropd  13342  grprcan  13413  isnsg3  13587  ghmpreima  13646  rngpropd  13761  ringpropd  13844  islmodd  14099  lmodprop2d  14154  lss1d  14189  epttop  14606  txdis1cn  14794  metequiv2  15012  cncfmptc  15112  cncfmptid  15113  addccncf  15116  negcncf  15121  dedekindicclemicc  15148  mpodvdsmulf1o  15506  2sqlem5  15640  2sqlem9  15645