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  7212  smo11  8298  zsupss  12854  lsmcv  21100  lspsolvlem  21101  mat2pmatghm  22678  mat2pmatmul  22679  nrmr0reg  23697  plyadd  26182  plymul  26183  coeeu  26190  ax5seglem6  28990  archiabl  33261  mdetpmtr1  33961  sseqval  34526  wsuclem  35998  btwnconn1lem1  36262  btwnconn1lem2  36263  btwnconn1lem12  36273  lshpsmreu  39406  1cvratlt  39771  llnle  39815  lvolex3N  39835  lnjatN  40077  lncvrat  40079  lncmp  40080  cdlemd6  40500  cdlemk19ylem  41227  pellex  43113  tfsconcatrn  43620  limcperiod  45910  itschlc0xyqsol1  49048  itschlc0xyqsol  49049