Theorem simp1rr 1258

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

Assertion

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

Proof of Theorem simp1rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1imass  7256  smo11  8350  zsupss  13034  lsmcv  21381  lspsolvlem  21382  mat2pmatghm  23010  mat2pmatmul  23011  nrmr0reg  24030  plyadd  26498  plymul  26499  coeeu  26506  ax5seglem6  29446  archiabl  33693  mdetpmtr1  34389  sseqval  34955  wsuclem  36509  btwnconn1lem1  36774  btwnconn1lem2  36775  btwnconn1lem12  36785  lshpsmreu  40086  1cvratlt  40451  llnle  40495  lvolex3N  40515  lnjatN  40757  lncvrat  40759  lncmp  40760  cdlemd6  41180  cdlemk19ylem  41907  pellex  43780  tfsconcatrn  44287  limcperiod  46562  nprmmul2  48532  itschlc0xyqsol1  49800  itschlc0xyqsol  49801