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 773	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1132	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  7284  smo11  8403  zsupss  12977  lsmcv  21161  lspsolvlem  21162  mat2pmatghm  22752  mat2pmatmul  22753  nrmr0reg  23773  plyadd  26271  plymul  26272  coeeu  26279  ax5seglem6  28964  archiabl  33188  mdetpmtr1  33784  sseqval  34370  wsuclem  35807  btwnconn1lem1  36069  btwnconn1lem2  36070  btwnconn1lem12  36080  lshpsmreu  39091  1cvratlt  39457  llnle  39501  lvolex3N  39521  lnjatN  39763  lncvrat  39765  lncmp  39766  cdlemd6  40186  cdlemk19ylem  40913  pellex  42823  tfsconcatrn  43332  limcperiod  45584  itschlc0xyqsol1  48616  itschlc0xyqsol  48617