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  5213  fcof1  5692  mpo0  5849  eroveu  6528  sbthlemi6  6858  sbthlemi8  6860  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  addcmpblnq0  7275  mulcmpblnq0  7276  nnnq0lem1  7278  prarloclemcalc  7334  addlocpr  7368  distrlem4prl  7416  distrlem4pru  7417  ltpopr  7427  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  prsrlem1  7574  ltsrprg  7579  apreap  8373  apreim  8389  divdivdivap  8497  divmuleqap  8501  divadddivap  8511  divsubdivap  8512  ledivdiv  8672  lediv12a  8676  exbtwnz  10059  seq3caopr  10287  leexp2r  10378  zfz1iso  10616  recvguniq  10799  rsqrmo  10831  summodclem2  11183  prodmodc  11379  qredeu  11814  pw2dvdseu  11882  epttop  12298  txdis1cn  12486  metequiv2  12704  mulc1cncf  12784  cncfmptc  12790  cncfmptid  12791  addccncf  12794  negcncf  12796  dedekindicclemicc  12818