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  7205  smo11  8294  zsupss  12856  lsmcv  21066  lspsolvlem  21067  mat2pmatghm  22633  mat2pmatmul  22634  nrmr0reg  23652  plyadd  26138  plymul  26139  coeeu  26146  ax5seglem6  28897  archiabl  33150  mdetpmtr1  33789  sseqval  34355  wsuclem  35798  btwnconn1lem1  36060  btwnconn1lem2  36061  btwnconn1lem12  36071  lshpsmreu  39087  1cvratlt  39453  llnle  39497  lvolex3N  39517  lnjatN  39759  lncvrat  39761  lncmp  39762  cdlemd6  40182  cdlemk19ylem  40909  pellex  42808  tfsconcatrn  43315  limcperiod  45610  itschlc0xyqsol1  48739  itschlc0xyqsol  48740