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  5340  fcof1  5830  mpo0  5992  eroveu  6685  sbthlemi6  7028  sbthlemi8  7030  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  addcmpblnq0  7510  mulcmpblnq0  7511  nnnq0lem1  7513  prarloclemcalc  7569  addlocpr  7603  distrlem4prl  7651  distrlem4pru  7652  ltpopr  7662  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  prsrlem1  7809  ltsrprg  7814  apreap  8614  apreim  8630  aptap  8677  divdivdivap  8740  divmuleqap  8744  divadddivap  8754  divsubdivap  8755  ledivdiv  8917  lediv12a  8921  exbtwnz  10340  seq3caopr  10587  seqcaoprg  10588  leexp2r  10685  zfz1iso  10933  recvguniq  11160  rsqrmo  11192  summodclem2  11547  prodmodc  11743  qredeu  12265  pw2dvdseu  12336  pcadd  12509  mhmpropd  13098  issubmd  13106  grprcan  13169  isnsg3  13337  ghmpreima  13396  rngpropd  13511  ringpropd  13594  lmodvsmmulgdi  13879  lmodprop2d  13904  lss1d  13939  epttop  14326  txdis1cn  14514  metequiv2  14732  mulc1cncf  14825  cncfmptc  14832  cncfmptid  14833  addccncf  14836  negcncf  14841  dedekindicclemicc  14868  mpodvdsmulf1o  15226  2sqlem5  15360  2sqlem9  15365