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  5437  fcof1  5955  mpo0  6122  eroveu  6859  sbthlemi6  7231  sbthlemi8  7233  suppeqfsuppbi  7247  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  addcmpblnq0  7754  mulcmpblnq0  7755  nnnq0lem1  7757  prarloclemcalc  7813  addlocpr  7847  distrlem4prl  7895  distrlem4pru  7896  ltpopr  7906  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  prsrlem1  8053  ltsrprg  8058  apreap  8857  apreim  8873  aptap  8920  divdivdivap  8983  divmuleqap  8987  divadddivap  8997  divsubdivap  8998  ledivdiv  9160  lediv12a  9164  exbtwnz  10606  seq3caopr  10853  seqcaoprg  10854  leexp2r  10951  zfz1iso  11206  ccatsymb  11283  wrd2ind  11408  swrdccat  11420  recvguniq  11673  rsqrmo  11705  summodclem2  12061  prodmodc  12257  qredeu  12787  pw2dvdseu  12858  pcadd  13031  mhmpropd  13668  issubmd  13676  grprcan  13739  isnsg3  13913  ghmpreima  13972  rngpropd  14088  ringpropd  14171  lmodvsmmulgdi  14458  lmodprop2d  14483  lss1d  14518  epttop  14942  txdis1cn  15130  metequiv2  15348  mulc1cncf  15441  cncfmptc  15448  cncfmptid  15449  addccncf  15452  negcncf  15457  dedekindicclemicc  15484  mpodvdsmulf1o  15845  2sqlem5  15979  2sqlem9  15984