Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1rr Structured version   Visualization version   GIF version

Theorem simp1rr 1120
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1rr (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 792 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1075 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  f1imass  6422  smo11  7348  zsupss  11653  lsmcv  18962  lspsolvlem  18963  mat2pmatghm  20354  mat2pmatmul  20355  nrmr0reg  21362  plyadd  23777  plymul  23778  coeeu  23785  ax5seglem6  25614  archiabl  29083  mdetpmtr1  29217  sseqval  29777  wsuclem  31017  wsuclemOLD  31018  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem12  31375  lshpsmreu  33414  1cvratlt  33778  llnle  33822  lvolex3N  33842  lnjatN  34084  lncvrat  34086  lncmp  34087  cdlemd6  34508  cdlemk19ylem  35236  pellex  36417  limcperiod  38695  clwwnisshclwwsn  41237
 Copyright terms: Public domain W3C validator