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  5409  fcof1  5919  mpo0  6086  eroveu  6790  sbthlemi6  7155  sbthlemi8  7157  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  addcmpblnq0  7656  mulcmpblnq0  7657  nnnq0lem1  7659  prarloclemcalc  7715  addlocpr  7749  distrlem4prl  7797  distrlem4pru  7798  ltpopr  7808  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  prsrlem1  7955  ltsrprg  7960  apreap  8760  apreim  8776  aptap  8823  divdivdivap  8886  divmuleqap  8890  divadddivap  8900  divsubdivap  8901  ledivdiv  9063  lediv12a  9067  exbtwnz  10503  seq3caopr  10750  seqcaoprg  10751  leexp2r  10848  zfz1iso  11098  ccatsymb  11172  wrd2ind  11297  swrdccat  11309  recvguniq  11549  rsqrmo  11581  summodclem2  11936  prodmodc  12132  qredeu  12662  pw2dvdseu  12733  pcadd  12906  mhmpropd  13542  issubmd  13550  grprcan  13613  isnsg3  13787  ghmpreima  13846  rngpropd  13961  ringpropd  14044  lmodvsmmulgdi  14330  lmodprop2d  14355  lss1d  14390  epttop  14807  txdis1cn  14995  metequiv2  15213  mulc1cncf  15306  cncfmptc  15313  cncfmptid  15314  addccncf  15317  negcncf  15322  dedekindicclemicc  15349  mpodvdsmulf1o  15707  2sqlem5  15841  2sqlem9  15846