Theorem simprll 526

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 481	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  5200  fcof1  5677  mpo0  5834  eroveu  6513  sbthlemi6  6843  sbthlemi8  6845  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  addcmpblnq0  7244  mulcmpblnq0  7245  nnnq0lem1  7247  prarloclemcalc  7303  addlocpr  7337  distrlem4prl  7385  distrlem4pru  7386  ltpopr  7396  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  prsrlem1  7543  ltsrprg  7548  apreap  8342  apreim  8358  divdivdivap  8466  divmuleqap  8470  divadddivap  8480  divsubdivap  8481  ledivdiv  8641  lediv12a  8645  exbtwnz  10021  seq3caopr  10249  leexp2r  10340  zfz1iso  10577  recvguniq  10760  rsqrmo  10792  summodclem2  11144  qredeu  11767  pw2dvdseu  11835  epttop  12248  txdis1cn  12436  metequiv2  12654  mulc1cncf  12734  cncfmptc  12740  cncfmptid  12741  addccncf  12744  negcncf  12746  dedekindicclemicc  12768