Theorem simp1rr 1235

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1imass  7024  smo11  8003  zsupss  12340  lsmcv  19915  lspsolvlem  19916  mat2pmatghm  21340  mat2pmatmul  21341  nrmr0reg  22359  plyadd  24809  plymul  24810  coeeu  24817  ax5seglem6  26722  archiabl  30829  mdetpmtr1  31090  sseqval  31648  wsuclem  33114  btwnconn1lem1  33550  btwnconn1lem2  33551  btwnconn1lem12  33561  lshpsmreu  36247  1cvratlt  36612  llnle  36656  lvolex3N  36676  lnjatN  36918  lncvrat  36920  lncmp  36921  cdlemd6  37341  cdlemk19ylem  38068  pellex  39439  limcperiod  41916  itschlc0xyqsol1  44760  itschlc0xyqsol  44761