Theorem simp1rr 1246

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1rr	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Proof of Theorem simp1rr

Step	Hyp	Ref	Expression
1		simprr 778	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1139	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1imass  7215  smo11  8301  zsupss  12885  lsmcv  21141  lspsolvlem  21142  mat2pmatghm  22720  mat2pmatmul  22721  nrmr0reg  23739  plyadd  26207  plymul  26208  coeeu  26215  ax5seglem6  29028  archiabl  33286  mdetpmtr1  34014  sseqval  34579  wsuclem  36052  btwnconn1lem1  36316  btwnconn1lem2  36317  btwnconn1lem12  36327  lshpsmreu  39602  1cvratlt  39967  llnle  40011  lvolex3N  40031  lnjatN  40273  lncvrat  40275  lncmp  40276  cdlemd6  40696  cdlemk19ylem  41423  pellex  43281  tfsconcatrn  43788  limcperiod  46074  nprmmul2  48004  itschlc0xyqsol1  49258  itschlc0xyqsol  49259