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

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

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 790 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1164 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  f1imass  6747  smo11  7698  zsupss  12018  lsmcv  19460  lspsolvlem  19461  mat2pmatghm  20860  mat2pmatmul  20861  nrmr0reg  21878  plyadd  24311  plymul  24312  coeeu  24319  ax5seglem6  26163  archiabl  30260  mdetpmtr1  30397  sseqval  30959  wsuclem  32275  btwnconn1lem1  32699  btwnconn1lem2  32700  btwnconn1lem12  32710  lshpsmreu  35122  1cvratlt  35487  llnle  35531  lvolex3N  35551  lnjatN  35793  lncvrat  35795  lncmp  35796  cdlemd6  36216  cdlemk19ylem  36943  pellex  38173  limcperiod  40592
  Copyright terms: Public domain W3C validator