Theorem simp1rr 1240

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1imass  7242  smo11  8336  zsupss  12903  lsmcv  21058  lspsolvlem  21059  mat2pmatghm  22624  mat2pmatmul  22625  nrmr0reg  23643  plyadd  26129  plymul  26130  coeeu  26137  ax5seglem6  28868  archiabl  33159  mdetpmtr1  33820  sseqval  34386  wsuclem  35820  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem12  36093  lshpsmreu  39109  1cvratlt  39475  llnle  39519  lvolex3N  39539  lnjatN  39781  lncvrat  39783  lncmp  39784  cdlemd6  40204  cdlemk19ylem  40931  pellex  42830  tfsconcatrn  43338  limcperiod  45633  itschlc0xyqsol1  48759  itschlc0xyqsol  48760