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  5414  fcof1  5929  mpo0  6096  eroveu  6800  sbthlemi6  7166  sbthlemi8  7168  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  addcmpblnq0  7668  mulcmpblnq0  7669  nnnq0lem1  7671  prarloclemcalc  7727  addlocpr  7761  distrlem4prl  7809  distrlem4pru  7810  ltpopr  7820  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  prsrlem1  7967  ltsrprg  7972  apreap  8772  apreim  8788  aptap  8835  divdivdivap  8898  divmuleqap  8902  divadddivap  8912  divsubdivap  8913  ledivdiv  9075  lediv12a  9079  exbtwnz  10516  seq3caopr  10763  seqcaoprg  10764  leexp2r  10861  zfz1iso  11111  ccatsymb  11188  wrd2ind  11313  swrdccat  11325  recvguniq  11578  rsqrmo  11610  summodclem2  11966  prodmodc  12162  qredeu  12692  pw2dvdseu  12763  pcadd  12936  mhmpropd  13572  issubmd  13580  grprcan  13643  isnsg3  13817  ghmpreima  13876  rngpropd  13992  ringpropd  14075  lmodvsmmulgdi  14361  lmodprop2d  14386  lss1d  14421  epttop  14843  txdis1cn  15031  metequiv2  15249  mulc1cncf  15342  cncfmptc  15349  cncfmptid  15350  addccncf  15353  negcncf  15358  dedekindicclemicc  15385  mpodvdsmulf1o  15743  2sqlem5  15877  2sqlem9  15882