Theorem simp1rr 1147

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  f1imass  6561  smo11  7506  zsupss  11815  lsmcv  19189  lspsolvlem  19190  mat2pmatghm  20583  mat2pmatmul  20584  nrmr0reg  21600  plyadd  24018  plymul  24019  coeeu  24026  ax5seglem6  25859  archiabl  29880  mdetpmtr1  30017  sseqval  30578  wsuclem  31895  btwnconn1lem1  32319  btwnconn1lem2  32320  btwnconn1lem12  32330  lshpsmreu  34714  1cvratlt  35078  llnle  35122  lvolex3N  35142  lnjatN  35384  lncvrat  35386  lncmp  35387  cdlemd6  35808  cdlemk19ylem  36535  pellex  37716  limcperiod  40178