Theorem simp1rr 1239

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  7252  smo11  8372  zsupss  12945  lsmcv  21087  lspsolvlem  21088  mat2pmatghm  22653  mat2pmatmul  22654  nrmr0reg  23672  plyadd  26159  plymul  26160  coeeu  26167  ax5seglem6  28845  archiabl  33114  mdetpmtr1  33762  sseqval  34328  wsuclem  35764  btwnconn1lem1  36026  btwnconn1lem2  36027  btwnconn1lem12  36037  lshpsmreu  39048  1cvratlt  39414  llnle  39458  lvolex3N  39478  lnjatN  39720  lncvrat  39722  lncmp  39723  cdlemd6  40143  cdlemk19ylem  40870  pellex  42783  tfsconcatrn  43291  limcperiod  45587  itschlc0xyqsol1  48632  itschlc0xyqsol  48633