Theorem simp1rr 1249

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

Assertion

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

Proof of Theorem simp1rr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  f1imass  7237  smo11  8323  zsupss  12928  lsmcv  21184  lspsolvlem  21185  mat2pmatghm  22763  mat2pmatmul  22764  nrmr0reg  23782  plyadd  26250  plymul  26251  coeeu  26258  ax5seglem6  29074  archiabl  33332  mdetpmtr1  34074  sseqval  34639  wsuclem  36121  btwnconn1lem1  36385  btwnconn1lem2  36386  btwnconn1lem12  36396  lshpsmreu  39681  1cvratlt  40046  llnle  40090  lvolex3N  40110  lnjatN  40352  lncvrat  40354  lncmp  40355  cdlemd6  40775  cdlemk19ylem  41502  pellex  43360  tfsconcatrn  43867  limcperiod  46152  nprmmul2  48082  itschlc0xyqsol1  49336  itschlc0xyqsol  49337