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  7239  smo11  8333  zsupss  12896  lsmcv  21051  lspsolvlem  21052  mat2pmatghm  22617  mat2pmatmul  22618  nrmr0reg  23636  plyadd  26122  plymul  26123  coeeu  26130  ax5seglem6  28861  archiabl  33152  mdetpmtr1  33813  sseqval  34379  wsuclem  35813  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem12  36086  lshpsmreu  39102  1cvratlt  39468  llnle  39512  lvolex3N  39532  lnjatN  39774  lncvrat  39776  lncmp  39777  cdlemd6  40197  cdlemk19ylem  40924  pellex  42823  tfsconcatrn  43331  limcperiod  45626  itschlc0xyqsol1  48755  itschlc0xyqsol  48756