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

Theorem jctild 563
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 553 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  syl6an  565  anc2li  577  ordunidif  5672  isofrlem  6464  dfwe2  6846  orduniorsuc  6895  poxp  7149  fnse  7154  ssenen  7992  dffi3  8193  fpwwe2lem13  9316  zmulcl  11255  rpneg  11691  rexuz3  13878  cau3lem  13884  climrlim2  14068  o1rlimmul  14139  iseralt  14205  gcdzeq  15051  isprm3  15176  vdwnnlem2  15480  ablfaclem3  18251  epttop  20561  lmcnp  20856  dfcon2  20970  txcnp  21171  cmphaushmeo  21351  isfild  21410  cnpflf2  21552  flimfnfcls  21580  alexsubALT  21603  fgcfil  22791  bcthlem5  22846  ivthlem2  22941  ivthlem3  22942  dvfsumrlim  23511  plypf1  23685  axeuclidlem  25556  wwlknredwwlkn0  26017  wwlkextwrd  26018  wwlkextproplem1  26031  clwlkisclwwlklem2a1  26069  rusgranumwlklem1  26238  numclwwlkovf2ex  26375  extwwlkfab  26379  lnon0  26839  hstles  28276  mdsl1i  28366  atcveq0  28393  atcvat4i  28442  cdjreui  28477  issgon  29315  conpcon  30273  tfisg  30762  frmin  30785  outsideofrflx  31206  isbasisrelowllem1  32178  isbasisrelowllem2  32179  poimirlem3  32381  poimirlem29  32407  poimir  32411  heicant  32413  equivtotbnd  32546  ismtybndlem  32574  cvrat4  33546  linepsubN  33855  pmapsub  33871  osumcllem4N  34062  pexmidlem1N  34073  dochexmidlem1  35566  clcnvlem  36748  2reu1  39635  iccpartimp  39756  bgoldbwt  40000  bgoldbst  40001  usgr2wlkneq  40960  wwlksnredwwlkn0  41100  wwlksnextwrd  41101  wwlksnextproplem1  41113  clwlkclwwlklem2a1  41199  av-numclwwlkovf2ex  41515  av-extwwlkfab  41518
  Copyright terms: Public domain W3C validator