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  5336  fcof1  5826  mpo0  5988  eroveu  6680  sbthlemi6  7021  sbthlemi8  7023  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  addcmpblnq0  7503  mulcmpblnq0  7504  nnnq0lem1  7506  prarloclemcalc  7562  addlocpr  7596  distrlem4prl  7644  distrlem4pru  7645  ltpopr  7655  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  prsrlem1  7802  ltsrprg  7807  apreap  8606  apreim  8622  aptap  8669  divdivdivap  8732  divmuleqap  8736  divadddivap  8746  divsubdivap  8747  ledivdiv  8909  lediv12a  8913  exbtwnz  10319  seq3caopr  10566  seqcaoprg  10567  leexp2r  10664  zfz1iso  10912  recvguniq  11139  rsqrmo  11171  summodclem2  11525  prodmodc  11721  qredeu  12235  pw2dvdseu  12306  pcadd  12478  mhmpropd  13038  issubmd  13046  grprcan  13109  isnsg3  13277  ghmpreima  13336  rngpropd  13451  ringpropd  13534  lmodvsmmulgdi  13819  lmodprop2d  13844  lss1d  13879  epttop  14258  txdis1cn  14446  metequiv2  14664  mulc1cncf  14744  cncfmptc  14750  cncfmptid  14751  addccncf  14754  negcncf  14759  dedekindicclemicc  14786  2sqlem5  15206  2sqlem9  15211