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  7252  smo11  8339  zsupss  12952  lsmcv  21234  lspsolvlem  21235  mat2pmatghm  22848  mat2pmatmul  22849  nrmr0reg  23867  plyadd  26335  plymul  26336  coeeu  26343  ax5seglem6  29193  archiabl  33431  mdetpmtr1  34130  sseqval  34695  wsuclem  36186  btwnconn1lem1  36450  btwnconn1lem2  36451  btwnconn1lem12  36461  lshpsmreu  39745  1cvratlt  40110  llnle  40154  lvolex3N  40174  lnjatN  40416  lncvrat  40418  lncmp  40419  cdlemd6  40839  cdlemk19ylem  41566  pellex  43424  tfsconcatrn  43931  limcperiod  46202  nprmmul2  48132  itschlc0xyqsol1  49397  itschlc0xyqsol  49398