Theorem simp1rr 1238

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1imass  7130  smo11  8183  zsupss  12665  lsmcv  20391  lspsolvlem  20392  mat2pmatghm  21867  mat2pmatmul  21868  nrmr0reg  22888  plyadd  25366  plymul  25367  coeeu  25374  ax5seglem6  27290  archiabl  31438  mdetpmtr1  31759  sseqval  32341  wsuclem  33805  btwnconn1lem1  34375  btwnconn1lem2  34376  btwnconn1lem12  34386  lshpsmreu  37109  1cvratlt  37474  llnle  37518  lvolex3N  37538  lnjatN  37780  lncvrat  37782  lncmp  37783  cdlemd6  38203  cdlemk19ylem  38930  pellex  40643  limcperiod  43128  itschlc0xyqsol1  46068  itschlc0xyqsol  46069