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

Theorem jctild 528
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 515 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  anc2li  558  equvini  2473  2reu1  3880  ordunidif  6238  isofrlem  7092  dfwe2  7495  orduniorsuc  7544  poxp  7821  fnse  7826  ssenen  8690  dffi3  8894  fpwwe2lem13  10063  zmulcl  12030  rpneg  12420  rexuz3  14707  cau3lem  14713  climrlim2  14903  o1rlimmul  14974  iseralt  15040  gcdzeq  15901  isprm3  16026  vdwnnlem2  16331  ablfaclem3  19208  epttop  21616  lmcnp  21911  dfconn2  22026  txcnp  22227  cmphaushmeo  22407  isfild  22465  cnpflf2  22607  flimfnfcls  22635  alexsubALT  22658  fgcfil  23873  bcthlem5  23930  ivthlem2  24052  ivthlem3  24053  dvfsumrlim  24627  plypf1  24801  axeuclidlem  26747  usgr2wlkneq  27536  wwlksnredwwlkn0  27673  wwlksnextwrd  27674  clwlkclwwlklem2a1  27769  lnon0  28574  hstles  30007  mdsl1i  30097  atcveq0  30124  atcvat4i  30173  cdjreui  30208  issgon  31382  connpconn  32482  tfisg  33055  frpoinsg  33081  frmin  33084  outsideofrflx  33588  isbasisrelowllem1  34635  isbasisrelowllem2  34636  poimirlem3  34894  poimirlem29  34920  poimir  34924  heicant  34926  equivtotbnd  35055  ismtybndlem  35083  cvrat4  36578  linepsubN  36887  pmapsub  36903  osumcllem4N  37094  pexmidlem1N  37105  dochexmidlem1  38595  harval3  39902  clcnvlem  39981  iccpartimp  43576  sbgoldbwt  43941  sbgoldbst  43942  elsetrecslem  44800
  Copyright terms: Public domain W3C validator