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  7207  smo11  8293  zsupss  12845  lsmcv  21088  lspsolvlem  21089  mat2pmatghm  22655  mat2pmatmul  22656  nrmr0reg  23674  plyadd  26159  plymul  26160  coeeu  26167  ax5seglem6  28923  archiabl  33178  mdetpmtr1  33847  sseqval  34412  wsuclem  35878  btwnconn1lem1  36142  btwnconn1lem2  36143  btwnconn1lem12  36153  lshpsmreu  39218  1cvratlt  39583  llnle  39627  lvolex3N  39647  lnjatN  39889  lncvrat  39891  lncmp  39892  cdlemd6  40312  cdlemk19ylem  41039  pellex  42942  tfsconcatrn  43449  limcperiod  45742  itschlc0xyqsol1  48881  itschlc0xyqsol  48882