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

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

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 809 . 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  plyadd  24018  plymul  24019  coeeu  24026  aannenlem1  24128  logexprlim  24995  ax5seglem6  25859  ax5seg  25863  mdetpmtr1  30017  mdetpmtr2  30018  wsuclem  31895  btwnconn1lem2  32320  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem12  32330  lshpsmreu  34714  2llnmat  35128  lvolex3N  35142  lnjatN  35384  pclfinclN  35554  lhpat3  35650  cdlemd6  35808  cdlemfnid  36169  cdlemk19ylem  36535  dihlsscpre  36840  dih1dimb2  36847  dihglblem6  36946  pellex  37716  mullimc  40166  mullimcf  40173  limcperiod  40178  cncfshift  40405  cncfperiod  40410
 Copyright terms: Public domain W3C validator