Theorem simprll 527

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 482	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  imain  5270  fcof1  5751  mpo0  5912  eroveu  6592  sbthlemi6  6927  sbthlemi8  6929  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  prarloclemcalc  7443  addlocpr  7477  distrlem4prl  7525  distrlem4pru  7526  ltpopr  7536  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  prsrlem1  7683  ltsrprg  7688  apreap  8485  apreim  8501  divdivdivap  8609  divmuleqap  8613  divadddivap  8623  divsubdivap  8624  ledivdiv  8785  lediv12a  8789  exbtwnz  10186  seq3caopr  10418  leexp2r  10509  zfz1iso  10754  recvguniq  10937  rsqrmo  10969  summodclem2  11323  prodmodc  11519  qredeu  12029  pw2dvdseu  12100  pcadd  12271  epttop  12730  txdis1cn  12918  metequiv2  13136  mulc1cncf  13216  cncfmptc  13222  cncfmptid  13223  addccncf  13226  negcncf  13228  dedekindicclemicc  13250  2sqlem5  13595  2sqlem9  13600