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  5312  fcof1  5799  fliftfun  5812  sbthlemi6  6978  sbthlemi8  6980  addcmpblnq  7383  mulcmpblnq  7384  ordpipqqs  7390  enq0tr  7450  addcmpblnq0  7459  mulcmpblnq0  7460  nnnq0lem1  7462  addnq0mo  7463  mulnq0mo  7464  prarloclemcalc  7518  addlocpr  7552  distrlem4prl  7600  distrlem4pru  7601  addcmpblnr  7755  mulcmpblnrlemg  7756  mulcmpblnr  7757  prsrlem1  7758  addsrmo  7759  mulsrmo  7760  ltsrprg  7763  apreap  8561  apreim  8577  aptap  8624  divdivdivap  8687  divsubdivap  8702  ledivdiv  8864  lediv12a  8868  exbtwnz  10268  seq3caopr  10500  leexp2r  10591  zfz1iso  10838  recvguniq  11021  rsqrmo  11053  summodclem2  11407  prodmodclem2  11602  prodmodc  11603  qredeu  12114  pw2dvdseu  12185  pcadd  12356  mhmpropd  12883  grprcan  12946  isnsg3  13111  ghmpreima  13165  rngpropd  13269  ringpropd  13352  islmodd  13569  lmodprop2d  13624  lss1d  13659  epttop  13973  txdis1cn  14161  metequiv2  14379  cncfmptc  14465  cncfmptid  14466  addccncf  14469  negcncf  14471  dedekindicclemicc  14493  2sqlem5  14849  2sqlem9  14854