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  7210  smo11  8295  zsupss  12876  lsmcv  21129  lspsolvlem  21130  mat2pmatghm  22704  mat2pmatmul  22705  nrmr0reg  23723  plyadd  26194  plymul  26195  coeeu  26202  ax5seglem6  29022  archiabl  33279  mdetpmtr1  33988  sseqval  34553  wsuclem  36026  btwnconn1lem1  36290  btwnconn1lem2  36291  btwnconn1lem12  36301  lshpsmreu  39566  1cvratlt  39931  llnle  39975  lvolex3N  39995  lnjatN  40237  lncvrat  40239  lncmp  40240  cdlemd6  40660  cdlemk19ylem  41387  pellex  43278  tfsconcatrn  43785  limcperiod  46073  nprmmul2  47985  itschlc0xyqsol1  49239  itschlc0xyqsol  49240