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

Theorem jctl 561
Description: Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
Hypothesis
Ref Expression
jctl.1 𝜓
Assertion
Ref Expression
jctl (𝜑 → (𝜓𝜑))

Proof of Theorem jctl
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 jctl.1 . 2 𝜓
31, 2jctil 557 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:  mpanl1  711  mpanlr1  717  relop  5182  odi  7523  cdaun  8854  nn0n0n1ge2  11205  0mod  12518  expge1  12714  hashge2el2dif  13067  swrd2lsw  13489  4dvdseven  14893  ndvdsp1  14919  istrkg2ld  25076  cusgra3vnbpr  25760  constr2spthlem1  25890  2pthon  25898  constr3trllem2  25945  constr3pthlem1  25949  constr3pthlem2  25950  wlkiswwlk2  25991  ococin  27457  cmbr4i  27650  iundifdif  28569  nepss  30660  axextndbi  30760  ontopbas  31403  bj-elccinfty  32074  poimirlem16  32391  mblfinlem4  32415  ismblfin  32416  fiphp3d  36197  eelT01  37753  eel0T1  37754  un01  37833  dirkercncf  38797  nnsum3primes4  40002  wspthsnwspthsnon  41117  0wlkOns1  41284
  Copyright terms: Public domain W3C validator