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

Theorem jctild 526
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 513 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  anc2li  556  equvini  2472  2reu1  3880  ordunidif  6233  isofrlem  7082  dfwe2  7484  orduniorsuc  7533  poxp  7813  fnse  7818  ssenen  8680  dffi3  8884  fpwwe2lem13  10053  zmulcl  12020  rpneg  12411  rexuz3  14698  cau3lem  14704  climrlim2  14894  o1rlimmul  14965  iseralt  15031  gcdzeq  15892  isprm3  16017  vdwnnlem2  16322  ablfaclem3  19140  epttop  21547  lmcnp  21842  dfconn2  21957  txcnp  22158  cmphaushmeo  22338  isfild  22396  cnpflf2  22538  flimfnfcls  22566  alexsubALT  22589  fgcfil  23803  bcthlem5  23860  ivthlem2  23982  ivthlem3  23983  dvfsumrlim  24557  plypf1  24731  axeuclidlem  26676  usgr2wlkneq  27465  wwlksnredwwlkn0  27602  wwlksnextwrd  27603  clwlkclwwlklem2a1  27698  lnon0  28503  hstles  29936  mdsl1i  30026  atcveq0  30053  atcvat4i  30102  cdjreui  30137  issgon  31282  connpconn  32380  tfisg  32953  frpoinsg  32979  frmin  32982  outsideofrflx  33486  isbasisrelowllem1  34519  isbasisrelowllem2  34520  poimirlem3  34777  poimirlem29  34803  poimir  34807  heicant  34809  equivtotbnd  34939  ismtybndlem  34967  cvrat4  36461  linepsubN  36770  pmapsub  36786  osumcllem4N  36977  pexmidlem1N  36988  dochexmidlem1  38478  harval3  39784  clcnvlem  39863  iccpartimp  43424  sbgoldbwt  43789  sbgoldbst  43790  elsetrecslem  44699
  Copyright terms: Public domain W3C validator