Theorem simp1rr 1256

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  f1imass  7262  smo11  8350  zsupss  12960  lsmcv  21244  lspsolvlem  21245  mat2pmatghm  22866  mat2pmatmul  22867  nrmr0reg  23885  plyadd  26353  plymul  26354  coeeu  26361  ax5seglem6  29250  archiabl  33484  mdetpmtr1  34179  sseqval  34744  wsuclem  36281  btwnconn1lem1  36545  btwnconn1lem2  36546  btwnconn1lem12  36556  lshpsmreu  39851  1cvratlt  40216  llnle  40260  lvolex3N  40280  lnjatN  40522  lncvrat  40524  lncmp  40525  cdlemd6  40945  cdlemk19ylem  41672  pellex  43532  tfsconcatrn  44039  limcperiod  46314  nprmmul2  48244  itschlc0xyqsol1  49513  itschlc0xyqsol  49514