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

Theorem jctild 527
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 22 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 jctild.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3jcad 519 1  |-  ( ph  ->  ( ps  ->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anc2li  540  ee12an  1353  ax12olem1  1868  2eu1  2223  ordunidif  4440  reusv7OLD  4546  dfwe2  4573  orduniorsuc  4621  isofrlem  5837  poxp  6227  fnse  6232  ssenen  7035  dffi3  7184  fpwwe2lem13  8264  zmulcl  10066  rpneg  10383  rexuz3  11832  cau3lem  11838  climrlim2  12021  o1rlimmul  12092  iseralt  12157  gcdeq  12731  isprm3  12767  vdwnnlem2  13043  ablfaclem3  15322  epttop  16746  lmcnp  17032  dfcon2  17145  txcnp  17314  cmphaushmeo  17491  isfild  17553  cnpflf2  17695  flimfnfcls  17723  alexsubALT  17745  fgcfil  18697  bcthlem5  18750  ivthlem2  18812  ivthlem3  18813  dvfsumrlim  19378  plypf1  19594  lnon0  21376  hstles  22811  mdsl1i  22901  atcveq0  22928  atcvat4i  22977  cdjreui  23012  issgon  23484  conpcon  23766  tfisg  24204  frmin  24242  axeuclidlem  24590  outsideofrflx  24750  equivtotbnd  26502  equivbnd  26514  ismtybndlem  26530  2reu1  27964  cvrat4  29632  linepsubN  29941  pmapsub  29957  osumcllem4N  30148  pexmidlem1N  30159  dochexmidlem1  31650
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 177  df-an 360
  Copyright terms: Public domain W3C validator