Theorem simp1rr 1241

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1rr	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Proof of Theorem simp1rr

Step	Hyp	Ref	Expression
1		simprr 773	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1imass  7220  smo11  8306  zsupss  12862  lsmcv  21108  lspsolvlem  21109  mat2pmatghm  22686  mat2pmatmul  22687  nrmr0reg  23705  plyadd  26190  plymul  26191  coeeu  26198  ax5seglem6  29019  archiabl  33291  mdetpmtr1  34000  sseqval  34565  wsuclem  36036  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem12  36311  lshpsmreu  39474  1cvratlt  39839  llnle  39883  lvolex3N  39903  lnjatN  40145  lncvrat  40147  lncmp  40148  cdlemd6  40568  cdlemk19ylem  41295  pellex  43181  tfsconcatrn  43688  limcperiod  45977  itschlc0xyqsol1  49115  itschlc0xyqsol  49116