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  5406  fcof1  5916  mpo0  6083  eroveu  6786  sbthlemi6  7145  sbthlemi8  7147  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  addcmpblnq0  7646  mulcmpblnq0  7647  nnnq0lem1  7649  prarloclemcalc  7705  addlocpr  7739  distrlem4prl  7787  distrlem4pru  7788  ltpopr  7798  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  prsrlem1  7945  ltsrprg  7950  apreap  8750  apreim  8766  aptap  8813  divdivdivap  8876  divmuleqap  8880  divadddivap  8890  divsubdivap  8891  ledivdiv  9053  lediv12a  9057  exbtwnz  10487  seq3caopr  10734  seqcaoprg  10735  leexp2r  10832  zfz1iso  11081  ccatsymb  11155  wrd2ind  11276  swrdccat  11288  recvguniq  11527  rsqrmo  11559  summodclem2  11914  prodmodc  12110  qredeu  12640  pw2dvdseu  12711  pcadd  12884  mhmpropd  13520  issubmd  13528  grprcan  13591  isnsg3  13765  ghmpreima  13824  rngpropd  13939  ringpropd  14022  lmodvsmmulgdi  14308  lmodprop2d  14333  lss1d  14368  epttop  14785  txdis1cn  14973  metequiv2  15191  mulc1cncf  15284  cncfmptc  15291  cncfmptid  15292  addccncf  15295  negcncf  15300  dedekindicclemicc  15327  mpodvdsmulf1o  15685  2sqlem5  15819  2sqlem9  15824