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  1880  2eu1  2236  ordunidif  4456  reusv7OLD  4562  dfwe2  4589  orduniorsuc  4637  isofrlem  5853  poxp  6243  fnse  6248  ssenen  7051  dffi3  7200  fpwwe2lem13  8280  zmulcl  10082  rpneg  10399  rexuz3  11848  cau3lem  11854  climrlim2  12037  o1rlimmul  12108  iseralt  12173  gcdeq  12747  isprm3  12783  vdwnnlem2  13059  ablfaclem3  15338  epttop  16762  lmcnp  17048  dfcon2  17161  txcnp  17330  cmphaushmeo  17507  isfild  17569  cnpflf2  17711  flimfnfcls  17739  alexsubALT  17761  fgcfil  18713  bcthlem5  18766  ivthlem2  18828  ivthlem3  18829  dvfsumrlim  19394  plypf1  19610  lnon0  21392  hstles  22827  mdsl1i  22917  atcveq0  22944  atcvat4i  22993  cdjreui  23028  issgon  23499  conpcon  23781  tfisg  24275  frmin  24313  axeuclidlem  24662  outsideofrflx  24822  equivtotbnd  26605  equivbnd  26617  ismtybndlem  26633  2reu1  28067  cvrat4  30254  linepsubN  30563  pmapsub  30579  osumcllem4N  30770  pexmidlem1N  30781  dochexmidlem1  32272
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