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

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

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1102 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  f1imass  6561  smo11  7506  zsupss  11815  lsmcv  19189  lspsolvlem  19190  mat2pmatghm  20583  mat2pmatmul  20584  nrmr0reg  21600  plyadd  24018  plymul  24019  coeeu  24026  ax5seglem6  25859  archiabl  29880  mdetpmtr1  30017  sseqval  30578  wsuclem  31895  btwnconn1lem1  32319  btwnconn1lem2  32320  btwnconn1lem12  32330  lshpsmreu  34714  1cvratlt  35078  llnle  35122  lvolex3N  35142  lnjatN  35384  lncvrat  35386  lncmp  35387  cdlemd6  35808  cdlemk19ylem  36535  pellex  37716  limcperiod  40178
  Copyright terms: Public domain W3C validator