Theorem simprll 537

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  5317  fcof1  5804  mpo0  5965  eroveu  6651  sbthlemi6  6990  sbthlemi8  6992  addcmpblnq  7395  mulcmpblnq  7396  ordpipqqs  7402  addcmpblnq0  7471  mulcmpblnq0  7472  nnnq0lem1  7474  prarloclemcalc  7530  addlocpr  7564  distrlem4prl  7612  distrlem4pru  7613  ltpopr  7623  addcmpblnr  7767  mulcmpblnrlemg  7768  mulcmpblnr  7769  prsrlem1  7770  ltsrprg  7775  apreap  8573  apreim  8589  aptap  8636  divdivdivap  8699  divmuleqap  8703  divadddivap  8713  divsubdivap  8714  ledivdiv  8876  lediv12a  8880  exbtwnz  10280  seq3caopr  10513  leexp2r  10604  zfz1iso  10852  recvguniq  11035  rsqrmo  11067  summodclem2  11421  prodmodc  11617  qredeu  12128  pw2dvdseu  12199  pcadd  12371  mhmpropd  12915  issubmd  12923  grprcan  12978  isnsg3  13143  ghmpreima  13202  rngpropd  13306  ringpropd  13389  lmodvsmmulgdi  13636  lmodprop2d  13661  lss1d  13696  epttop  14042  txdis1cn  14230  metequiv2  14448  mulc1cncf  14528  cncfmptc  14534  cncfmptid  14535  addccncf  14538  negcncf  14540  dedekindicclemicc  14562  2sqlem5  14919  2sqlem9  14924