Theorem simp1rr 1257

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

Assertion

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

Proof of Theorem simp1rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  f1imass  7262  smo11  8349  zsupss  12967  lsmcv  21276  lspsolvlem  21277  mat2pmatghm  22898  mat2pmatmul  22899  nrmr0reg  23917  plyadd  26385  plymul  26386  coeeu  26393  ax5seglem6  29295  archiabl  33527  mdetpmtr1  34222  sseqval  34787  wsuclem  36323  btwnconn1lem1  36587  btwnconn1lem2  36588  btwnconn1lem12  36598  lshpsmreu  39911  1cvratlt  40276  llnle  40320  lvolex3N  40340  lnjatN  40582  lncvrat  40584  lncmp  40585  cdlemd6  41005  cdlemk19ylem  41732  pellex  43590  tfsconcatrn  44097  limcperiod  46372  nprmmul2  48305  itschlc0xyqsol1  49574  itschlc0xyqsol  49575