Theorem simprll 539

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 109	. 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  5443  fcof1  5962  mpo0  6131  eroveu  6873  sbthlemi6  7245  sbthlemi8  7247  suppeqfsuppbi  7261  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prarloclemcalc  7833  addlocpr  7867  distrlem4prl  7915  distrlem4pru  7916  ltpopr  7926  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  ltsrprg  8078  apreap  8879  apreim  8895  aptap  8942  divdivdivap  9007  divmuleqap  9011  divadddivap  9021  divsubdivap  9022  ledivdiv  9184  lediv12a  9188  exbtwnz  10637  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  zfz1iso  11241  ccatsymb  11318  wrd2ind  11443  swrdccat  11455  recvguniq  11708  rsqrmo  11740  summodclem2  12096  prodmodc  12292  qredeu  12822  pw2dvdseu  12893  pcadd  13066  mhmpropd  13724  issubmd  13732  grprcan  13795  isnsg3  13963  ghmpreima  14022  rngpropd  14197  ringpropd  14284  lmodvsmmulgdi  14600  lmodprop2d  14625  lss1d  14660  epttop  15084  txdis1cn  15272  metequiv2  15490  mulc1cncf  15583  cncfmptc  15590  cncfmptid  15591  addccncf  15594  negcncf  15599  dedekindicclemicc  15626  mpodvdsmulf1o  15987  2sqlem5  16121  2sqlem9  16126