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  5831  fliftfun  5844  sbthlemi6  7029  sbthlemi8  7031  addcmpblnq  7436  mulcmpblnq  7437  ordpipqqs  7443  enq0tr  7503  addcmpblnq0  7512  mulcmpblnq0  7513  nnnq0lem1  7515  addnq0mo  7516  mulnq0mo  7517  prarloclemcalc  7571  addlocpr  7605  distrlem4prl  7653  distrlem4pru  7654  addcmpblnr  7808  mulcmpblnrlemg  7809  mulcmpblnr  7810  prsrlem1  7811  addsrmo  7812  mulsrmo  7813  ltsrprg  7816  apreap  8616  apreim  8632  aptap  8679  divdivdivap  8742  divsubdivap  8757  ledivdiv  8919  lediv12a  8923  exbtwnz  10342  seq3caopr  10589  seqcaoprg  10590  leexp2r  10687  zfz1iso  10935  recvguniq  11162  rsqrmo  11194  summodclem2  11549  prodmodclem2  11744  prodmodc  11745  qredeu  12275  pw2dvdseu  12346  pcadd  12519  mhmpropd  13108  grprcan  13179  isnsg3  13347  ghmpreima  13406  rngpropd  13521  ringpropd  13604  islmodd  13859  lmodprop2d  13914  lss1d  13949  epttop  14336  txdis1cn  14524  metequiv2  14742  cncfmptc  14842  cncfmptid  14843  addccncf  14846  negcncf  14851  dedekindicclemicc  14878  mpodvdsmulf1o  15236  2sqlem5  15370  2sqlem9  15375