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 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  imain  5466  fcof1  5992  mpo0  6161  eroveu  6904  sbthlemi6  7285  sbthlemi8  7287  suppeqfsuppbi  7301  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  addcmpblnq0  7817  mulcmpblnq0  7818  nnnq0lem1  7820  prarloclemcalc  7876  addlocpr  7910  distrlem4prl  7958  distrlem4pru  7959  ltpopr  7969  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  ltsrprg  8121  apreap  8924  apreim  8940  aptap  8987  divdivdivap  9052  divmuleqap  9056  divadddivap  9066  divsubdivap  9067  ledivdiv  9229  lediv12a  9233  exbtwnz  10703  seq3caopr  10954  seqcaoprg  10955  leexp2r  11052  hashf1lem1  11308  hashf1lem2  11309  zfz1iso  11316  ccatsymb  11393  wrd2ind  11518  swrdccat  11530  recvguniq  11784  rsqrmo  11816  summodclem2  12175  prodmodc  12371  qredeu  12901  pwbdvdseu  12973  pcadd  13149  mhmpropd  13833  issubmd  13841  grprcan  13902  isnsg3  14070  ghmpreima  14129  rngpropd  14362  ringpropd  14451  lmodvsmmulgdi  14770  lmodprop2d  14795  lss1d  14830  assamulgscmlem2  15152  mvrf1fi  15215  epttop  15328  txdis1cn  15516  metequiv2  15734  mulc1cncf  15827  cncfmptc  15834  cncfmptid  15835  addccncf  15838  negcncf  15843  dedekindicclemicc  15870  mpodvdsmulf1o  16296  2sqlem5  16455  2sqlem9  16460