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

Theorem jctild 543
 Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
Hypotheses
Ref Expression
jctild.1
jctild.2
Assertion
Ref Expression
jctild

Proof of Theorem jctild
StepHypRef Expression
1 jctild.2 . . 3
21a1d 25 . 2
3 jctild.1 . 2
42, 3jcad 533 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  syl6an  545  anc2li  557  ifpfal  1389  2eu1OLD  2377  reusv7OLD  4664  ordunidif  4931  isofrlem  6236  dfwe2  6617  orduniorsuc  6665  poxp  6912  fnse  6917  ssenen  7711  dffi3  7911  fpwwe2lem13  9041  zmulcl  10937  rpneg  11278  rexuz3  13181  cau3lem  13187  climrlim2  13370  o1rlimmul  13441  iseralt  13507  gcdeq  14190  isprm3  14226  vdwnnlem2  14514  ablfaclem3  17138  epttop  19510  lmcnp  19805  dfcon2  19920  txcnp  20121  cmphaushmeo  20301  isfild  20359  cnpflf2  20501  flimfnfcls  20529  alexsubALT  20551  fgcfil  21710  bcthlem5  21767  ivthlem2  21864  ivthlem3  21865  dvfsumrlim  22432  plypf1  22609  axeuclidlem  24265  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkextproplem1  24741  clwlkisclwwlklem2a1  24779  rusgranumwlklem1  24949  numclwwlkovf2ex  25086  extwwlkfab  25090  lnon0  25713  hstles  27150  mdsl1i  27240  atcveq0  27267  atcvat4i  27316  cdjreui  27351  issgon  28123  conpcon  28680  tfisg  29284  frmin  29322  outsideofrflx  29777  heicant  30049  equivtotbnd  30274  ismtybndlem  30302  2reu1  32191  cvrat4  35167  linepsubN  35476  pmapsub  35492  osumcllem4N  35683  pexmidlem1N  35694  dochexmidlem1  37187 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