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  5205  fcof1  5684  mpo0  5841  eroveu  6520  sbthlemi6  6850  sbthlemi8  6852  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  addcmpblnq0  7251  mulcmpblnq0  7252  nnnq0lem1  7254  prarloclemcalc  7310  addlocpr  7344  distrlem4prl  7392  distrlem4pru  7393  ltpopr  7403  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  prsrlem1  7550  ltsrprg  7555  apreap  8349  apreim  8365  divdivdivap  8473  divmuleqap  8477  divadddivap  8487  divsubdivap  8488  ledivdiv  8648  lediv12a  8652  exbtwnz  10028  seq3caopr  10256  leexp2r  10347  zfz1iso  10584  recvguniq  10767  rsqrmo  10799  summodclem2  11151  prodmodc  11347  qredeu  11778  pw2dvdseu  11846  epttop  12259  txdis1cn  12447  metequiv2  12665  mulc1cncf  12745  cncfmptc  12751  cncfmptid  12752  addccncf  12755  negcncf  12757  dedekindicclemicc  12779