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  7268  smo11  8373  zsupss  13065  lsmcv  21420  lspsolvlem  21421  mat2pmatghm  23049  mat2pmatmul  23050  nrmr0reg  24069  plyadd  26537  plymul  26538  coeeu  26545  ax5seglem6  29513  archiabl  33802  mdetpmtr1  34498  sseqval  35063  wsuclem  36662  btwnconn1lem1  36927  btwnconn1lem2  36928  btwnconn1lem12  36938  lshpsmreu  40242  1cvratlt  40607  llnle  40651  lvolex3N  40671  lnjatN  40913  lncvrat  40915  lncmp  40916  cdlemd6  41336  cdlemk19ylem  42063  pellex  43918  tfsconcatrn  44420  limcperiod  46716  nprmmul2  48686  itschlc0xyqsol1  49954  itschlc0xyqsol  49955