Theorem simprll 543

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 494	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  5461  fcof1  5983  mpo0  6152  eroveu  6894  sbthlemi6  7273  sbthlemi8  7275  suppeqfsuppbi  7289  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  addcmpblnq0  7804  mulcmpblnq0  7805  nnnq0lem1  7807  prarloclemcalc  7863  addlocpr  7897  distrlem4prl  7945  distrlem4pru  7946  ltpopr  7956  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  prsrlem1  8103  ltsrprg  8108  apreap  8909  apreim  8925  aptap  8972  divdivdivap  9037  divmuleqap  9041  divadddivap  9051  divsubdivap  9052  ledivdiv  9214  lediv12a  9218  exbtwnz  10668  seq3caopr  10915  seqcaoprg  10916  leexp2r  11013  hashf1lem1  11268  hashf1lem2  11269  zfz1iso  11276  ccatsymb  11353  wrd2ind  11478  swrdccat  11490  recvguniq  11744  rsqrmo  11776  summodclem2  12132  prodmodc  12328  qredeu  12858  pw2dvdseu  12929  pcadd  13102  mhmpropd  13756  issubmd  13764  grprcan  13825  isnsg3  13993  ghmpreima  14052  rngpropd  14237  ringpropd  14326  lmodvsmmulgdi  14643  lmodprop2d  14668  lss1d  14703  assamulgscmlem2  15025  epttop  15174  txdis1cn  15362  metequiv2  15580  mulc1cncf  15673  cncfmptc  15680  cncfmptid  15681  addccncf  15684  negcncf  15689  dedekindicclemicc  15716  mpodvdsmulf1o  16087  2sqlem5  16221  2sqlem9  16226