Theorem simp1rr 1238

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1imass  7137  smo11  8195  zsupss  12677  lsmcv  20403  lspsolvlem  20404  mat2pmatghm  21879  mat2pmatmul  21880  nrmr0reg  22900  plyadd  25378  plymul  25379  coeeu  25386  ax5seglem6  27302  archiabl  31452  mdetpmtr1  31773  sseqval  32355  wsuclem  33819  btwnconn1lem1  34389  btwnconn1lem2  34390  btwnconn1lem12  34400  lshpsmreu  37123  1cvratlt  37488  llnle  37532  lvolex3N  37552  lnjatN  37794  lncvrat  37796  lncmp  37797  cdlemd6  38217  cdlemk19ylem  38944  pellex  40657  limcperiod  43169  itschlc0xyqsol1  46112  itschlc0xyqsol  46113