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

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

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 767 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1127 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  f1imass  7019  smo11  7995  zsupss  12329  lsmcv  19835  lspsolvlem  19836  mat2pmatghm  21254  mat2pmatmul  21255  plyadd  24722  plymul  24723  coeeu  24730  aannenlem1  24832  logexprlim  25715  ax5seglem6  26635  ax5seg  26639  mdetpmtr1  30975  mdetpmtr2  30976  wsuclem  32997  btwnconn1lem2  33434  btwnconn1lem3  33435  btwnconn1lem4  33436  btwnconn1lem12  33444  lshpsmreu  36113  2llnmat  36528  lvolex3N  36542  lnjatN  36784  pclfinclN  36954  lhpat3  37050  cdlemd6  37207  cdlemfnid  37568  cdlemk19ylem  37934  dihlsscpre  38238  dih1dimb2  38245  dihglblem6  38344  pellex  39294  mullimc  41759  mullimcf  41766  limcperiod  41771  cncfshift  42019  cncfperiod  42024
  Copyright terms: Public domain W3C validator