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  7264  smo11  8356  zsupss  12989  lsmcv  21332  lspsolvlem  21333  mat2pmatghm  22959  mat2pmatmul  22960  nrmr0reg  23979  plyadd  26447  plymul  26448  coeeu  26455  ax5seglem6  29392  archiabl  33640  mdetpmtr1  34335  sseqval  34901  wsuclem  36404  btwnconn1lem1  36669  btwnconn1lem2  36670  btwnconn1lem12  36680  lshpsmreu  39984  1cvratlt  40349  llnle  40393  lvolex3N  40413  lnjatN  40655  lncvrat  40657  lncmp  40658  cdlemd6  41078  cdlemk19ylem  41805  pellex  43678  tfsconcatrn  44185  limcperiod  46460  nprmmul2  48430  itschlc0xyqsol1  49698  itschlc0xyqsol  49699