Theorem simp1rr 1240

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

Assertion

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

Proof of Theorem simp1rr

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

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

This theorem is referenced by:  f1imass  7257  smo11  8378  zsupss  12953  lsmcv  21102  lspsolvlem  21103  mat2pmatghm  22668  mat2pmatmul  22669  nrmr0reg  23687  plyadd  26174  plymul  26175  coeeu  26182  ax5seglem6  28913  archiabl  33196  mdetpmtr1  33854  sseqval  34420  wsuclem  35843  btwnconn1lem1  36105  btwnconn1lem2  36106  btwnconn1lem12  36116  lshpsmreu  39127  1cvratlt  39493  llnle  39537  lvolex3N  39557  lnjatN  39799  lncvrat  39801  lncmp  39802  cdlemd6  40222  cdlemk19ylem  40949  pellex  42858  tfsconcatrn  43366  limcperiod  45657  itschlc0xyqsol1  48746  itschlc0xyqsol  48747