Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  expl Unicode version

Theorem expl 618
 Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
Hypothesis
Ref Expression
expl.1
Assertion
Ref Expression
expl

Proof of Theorem expl
StepHypRef Expression
1 expl.1 . . 3
21exp31 604 . 2
32impd 431 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  reximd2a  2927  tfindsg2  6696  tz7.49c  7130  ssenen  7711  pssnn  7758  unwdomg  8031  cff1  8659  cfsmolem  8671  cfpwsdom  8980  wunex2  9137  mulgt0sr  9503  uzwo  11173  uzwoOLD  11174  shftfval  12903  fsum2dlem  13585  fprod2dlem  13784  prmpwdvds  14422  quscrng  17888  chfacfscmul0  19359  chfacfpmmul0  19363  tgtop  19475  neitr  19681  bwth  19910  tx1stc  20151  cnextcn  20567  logfac2  23492  axcontlem12  24278  spanuni  26462  pjnmopi  27067  superpos  27273  atcvat4i  27316  fpwrelmap  27556  2sqmo  27637  locfinreflem  27843  cmpcref  27853  fin2so  30040  heicant  30049  ismblfin  30055  ovoliunnfl  30056  itg2gt0cn  30070  fneint  30166  neibastop3  30180  pell14qrexpcl  30803  cvrat4  35167 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 185  df-an 371
 Copyright terms: Public domain W3C validator