Theorem simp1rr 1241

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1imass  7219  smo11  8304  zsupss  12887  lsmcv  21139  lspsolvlem  21140  mat2pmatghm  22695  mat2pmatmul  22696  nrmr0reg  23714  plyadd  26182  plymul  26183  coeeu  26190  ax5seglem6  29003  archiabl  33259  mdetpmtr1  33967  sseqval  34532  wsuclem  36005  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem12  36280  lshpsmreu  39555  1cvratlt  39920  llnle  39964  lvolex3N  39984  lnjatN  40226  lncvrat  40228  lncmp  40229  cdlemd6  40649  cdlemk19ylem  41376  pellex  43263  tfsconcatrn  43770  limcperiod  46058  nprmmul2  47982  itschlc0xyqsol1  49236  itschlc0xyqsol  49237