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

Theorem jctl 516
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 512 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387
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 199  df-an 388
This theorem is referenced by:  mpanl1  688  mpanlr1  694  opeqsng  5245  relop  5567  odi  8004  endjudisj  9390  nn0n0n1ge2  11772  0mod  13083  expge1  13279  hashge2el2dif  13647  swrd2lsw  14174  4dvdseven  15582  ndvdsp1  15620  istrkg2ld  25963  clwlkclwwlkfOLD  27533  0wlkons1  27665  ococin  28981  cmbr4i  29174  iundifdif  30100  nepss  32505  axextndbi  32607  ontopbas  33333  bj-elccinfty  34002  ctbssinf  34165  poimirlem16  34386  mblfinlem4  34410  ismblfin  34411  fiphp3d  38850  eelT01  40501  eel0T1  40502  un01  40579  dirkercncf  41855  nnsum3primes4  43353  line2x  44141  line2y  44142
  Copyright terms: Public domain W3C validator