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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  f1imass  7265  smo11  8366  zsupss  12925  lsmcv  20899  lspsolvlem  20900  mat2pmatghm  22452  mat2pmatmul  22453  nrmr0reg  23473  plyadd  25966  plymul  25967  coeeu  25974  ax5seglem6  28459  archiabl  32614  mdetpmtr1  33101  sseqval  33685  wsuclem  35101  btwnconn1lem1  35363  btwnconn1lem2  35364  btwnconn1lem12  35374  lshpsmreu  38282  1cvratlt  38648  llnle  38692  lvolex3N  38712  lnjatN  38954  lncvrat  38956  lncmp  38957  cdlemd6  39377  cdlemk19ylem  40104  pellex  41875  tfsconcatrn  42394  limcperiod  44642  itschlc0xyqsol1  47539  itschlc0xyqsol  47540