Theorem simp1rr 1237

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 1131	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  f1imass  7274  smo11  8385  zsupss  12952  lsmcv  21029  lspsolvlem  21030  mat2pmatghm  22645  mat2pmatmul  22646  nrmr0reg  23666  plyadd  26164  plymul  26165  coeeu  26172  ax5seglem6  28758  archiabl  32919  mdetpmtr1  33424  sseqval  34008  wsuclem  35421  btwnconn1lem1  35683  btwnconn1lem2  35684  btwnconn1lem12  35694  lshpsmreu  38581  1cvratlt  38947  llnle  38991  lvolex3N  39011  lnjatN  39253  lncvrat  39255  lncmp  39256  cdlemd6  39676  cdlemk19ylem  40403  pellex  42255  tfsconcatrn  42771  limcperiod  45016  itschlc0xyqsol1  47839  itschlc0xyqsol  47840