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  5403  fcof1  5913  fliftfun  5926  sbthlemi6  7137  sbthlemi8  7139  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  enq0tr  7629  addcmpblnq0  7638  mulcmpblnq0  7639  nnnq0lem1  7641  addnq0mo  7642  mulnq0mo  7643  prarloclemcalc  7697  addlocpr  7731  distrlem4prl  7779  distrlem4pru  7780  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  prsrlem1  7937  addsrmo  7938  mulsrmo  7939  ltsrprg  7942  apreap  8742  apreim  8758  aptap  8805  divdivdivap  8868  divsubdivap  8883  ledivdiv  9045  lediv12a  9049  exbtwnz  10478  seq3caopr  10725  seqcaoprg  10726  leexp2r  10823  zfz1iso  11071  wrd2ind  11263  swrdccat  11275  recvguniq  11514  rsqrmo  11546  summodclem2  11901  prodmodclem2  12096  prodmodc  12097  qredeu  12627  pw2dvdseu  12698  pcadd  12871  mhmpropd  13507  grprcan  13578  isnsg3  13752  ghmpreima  13811  rngpropd  13926  ringpropd  14009  islmodd  14265  lmodprop2d  14320  lss1d  14355  epttop  14772  txdis1cn  14960  metequiv2  15178  cncfmptc  15278  cncfmptid  15279  addccncf  15282  negcncf  15287  dedekindicclemicc  15314  mpodvdsmulf1o  15672  2sqlem5  15806  2sqlem9  15811