Theorem simp1rr 1237

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  f1imass  7118  smo11  8166  zsupss  12606  lsmcv  20318  lspsolvlem  20319  mat2pmatghm  21787  mat2pmatmul  21788  nrmr0reg  22808  plyadd  25283  plymul  25284  coeeu  25291  ax5seglem6  27205  archiabl  31354  mdetpmtr1  31675  sseqval  32255  wsuclem  33746  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem12  34327  lshpsmreu  37050  1cvratlt  37415  llnle  37459  lvolex3N  37479  lnjatN  37721  lncvrat  37723  lncmp  37724  cdlemd6  38144  cdlemk19ylem  38871  pellex  40573  limcperiod  43059  itschlc0xyqsol1  46000  itschlc0xyqsol  46001