Theorem simp1rr 1258

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

Assertion

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

Proof of Theorem simp1rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1imass  7291  smo11  8400  zsupss  13091  lsmcv  21449  lspsolvlem  21450  mat2pmatghm  23078  mat2pmatmul  23079  nrmr0reg  24098  plyadd  26566  plymul  26567  coeeu  26574  ax5seglem6  29542  archiabl  33829  mdetpmtr1  34525  sseqval  35090  wsuclem  36765  btwnconn1lem1  37030  btwnconn1lem2  37031  btwnconn1lem12  37041  lshpsmreu  40358  1cvratlt  40723  llnle  40767  lvolex3N  40787  lnjatN  41029  lncvrat  41031  lncmp  41032  cdlemd6  41452  cdlemk19ylem  42179  pellex  44035  tfsconcatrn  44536  limcperiod  46845  nprmmul2  48815  itschlc0xyqsol1  50083  itschlc0xyqsol  50084