Theorem simp1rr 1236

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 1130	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  f1imass  7000  smo11  7984  zsupss  12325  lsmcv  19906  lspsolvlem  19907  mat2pmatghm  21335  mat2pmatmul  21336  nrmr0reg  22354  plyadd  24814  plymul  24815  coeeu  24822  ax5seglem6  26728  archiabl  30877  mdetpmtr1  31176  sseqval  31756  wsuclem  33225  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem12  33672  lshpsmreu  36405  1cvratlt  36770  llnle  36814  lvolex3N  36834  lnjatN  37076  lncvrat  37078  lncmp  37079  cdlemd6  37499  cdlemk19ylem  38226  pellex  39776  limcperiod  42270  itschlc0xyqsol1  45180  itschlc0xyqsol  45181