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  7193  smo11  8279  zsupss  12827  lsmcv  21071  lspsolvlem  21072  mat2pmatghm  22638  mat2pmatmul  22639  nrmr0reg  23657  plyadd  26142  plymul  26143  coeeu  26150  ax5seglem6  28905  archiabl  33157  mdetpmtr1  33826  sseqval  34391  wsuclem  35838  btwnconn1lem1  36100  btwnconn1lem2  36101  btwnconn1lem12  36111  lshpsmreu  39127  1cvratlt  39492  llnle  39536  lvolex3N  39556  lnjatN  39798  lncvrat  39800  lncmp  39801  cdlemd6  40221  cdlemk19ylem  40948  pellex  42847  tfsconcatrn  43354  limcperiod  45647  itschlc0xyqsol1  48777  itschlc0xyqsol  48778