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

Theorem jctild 529
Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
Hypotheses
Ref Expression
jctild.1  |-  ( ph  ->  ( ps  ->  ch ) )
jctild.2  |-  ( ph  ->  th )
Assertion
Ref Expression
jctild  |-  ( ph  ->  ( ps  ->  ( th  /\  ch ) ) )

Proof of Theorem jctild
StepHypRef Expression
1 jctild.2 . . 3  |-  ( ph  ->  th )
21a1d 24 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 jctild.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3jcad 521 1  |-  ( ph  ->  ( ps  ->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  anc2li  542  ee12an  1373  ax12olem1OLD  2012  2eu1  2362  ordunidif  4630  reusv7OLD  4736  dfwe2  4763  orduniorsuc  4811  isofrlem  6061  poxp  6459  fnse  6464  ssenen  7282  dffi3  7437  fpwwe2lem13  8518  zmulcl  10325  rpneg  10642  rexuz3  12153  cau3lem  12159  climrlim2  12342  o1rlimmul  12413  iseralt  12479  gcdeq  13053  isprm3  13089  vdwnnlem2  13365  ablfaclem3  15646  epttop  17074  lmcnp  17369  dfcon2  17483  txcnp  17653  cmphaushmeo  17833  isfild  17891  cnpflf2  18033  flimfnfcls  18061  alexsubALT  18083  fgcfil  19225  bcthlem5  19282  ivthlem2  19350  ivthlem3  19351  dvfsumrlim  19916  plypf1  20132  lnon0  22300  hstles  23735  mdsl1i  23825  atcveq0  23852  atcvat4i  23901  cdjreui  23936  issgon  24507  conpcon  24923  tfisg  25480  frmin  25518  axeuclidlem  25902  outsideofrflx  26062  equivtotbnd  26488  ismtybndlem  26516  2reu1  27941  ccatsymb  28180  cvrat4  30241  linepsubN  30550  pmapsub  30566  osumcllem4N  30757  pexmidlem1N  30768  dochexmidlem1  32259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator