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  5337  fcof1  5827  mpo0  5989  eroveu  6682  sbthlemi6  7023  sbthlemi8  7025  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  addcmpblnq0  7505  mulcmpblnq0  7506  nnnq0lem1  7508  prarloclemcalc  7564  addlocpr  7598  distrlem4prl  7646  distrlem4pru  7647  ltpopr  7657  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  prsrlem1  7804  ltsrprg  7809  apreap  8608  apreim  8624  aptap  8671  divdivdivap  8734  divmuleqap  8738  divadddivap  8748  divsubdivap  8749  ledivdiv  8911  lediv12a  8915  exbtwnz  10322  seq3caopr  10569  seqcaoprg  10570  leexp2r  10667  zfz1iso  10915  recvguniq  11142  rsqrmo  11174  summodclem2  11528  prodmodc  11724  qredeu  12238  pw2dvdseu  12309  pcadd  12481  mhmpropd  13041  issubmd  13049  grprcan  13112  isnsg3  13280  ghmpreima  13339  rngpropd  13454  ringpropd  13537  lmodvsmmulgdi  13822  lmodprop2d  13847  lss1d  13882  epttop  14269  txdis1cn  14457  metequiv2  14675  mulc1cncf  14768  cncfmptc  14775  cncfmptid  14776  addccncf  14779  negcncf  14784  dedekindicclemicc  14811  2sqlem5  15276  2sqlem9  15281