Theorem simp1rr 1120

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1imass  6422  smo11  7348  zsupss  11653  lsmcv  18962  lspsolvlem  18963  mat2pmatghm  20354  mat2pmatmul  20355  nrmr0reg  21362  plyadd  23777  plymul  23778  coeeu  23785  ax5seglem6  25614  archiabl  29083  mdetpmtr1  29217  sseqval  29777  wsuclem  31017  wsuclemOLD  31018  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem12  31375  lshpsmreu  33414  1cvratlt  33778  llnle  33822  lvolex3N  33842  lnjatN  34084  lncvrat  34086  lncmp  34087  cdlemd6  34508  cdlemk19ylem  35236  pellex  36417  limcperiod  38695  clwwnisshclwwsn  41237