Theorem simp1rr 1321

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  f1imass  6747  smo11  7698  zsupss  12018  lsmcv  19460  lspsolvlem  19461  mat2pmatghm  20860  mat2pmatmul  20861  nrmr0reg  21878  plyadd  24311  plymul  24312  coeeu  24319  ax5seglem6  26163  archiabl  30260  mdetpmtr1  30397  sseqval  30959  wsuclem  32275  btwnconn1lem1  32699  btwnconn1lem2  32700  btwnconn1lem12  32710  lshpsmreu  35122  1cvratlt  35487  llnle  35531  lvolex3N  35551  lnjatN  35793  lncvrat  35795  lncmp  35796  cdlemd6  36216  cdlemk19ylem  36943  pellex  38173  limcperiod  40592