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

Theorem jctl 525
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 521 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  mpanl1  699  mpanlr1  705  opeqsng  5465  relop  5811  odi  8531  ssfi  9124  endjudisj  10111  nn0n0n1ge2  12487  0mod  13814  expge1  14012  hashge2el2dif  14386  swrdccatin2  14624  swrd2lsw  14848  4dvdseven  16262  ndvdsp1  16300  istrkg2ld  27444  0wlkons1  29107  ococin  30392  cmbr4i  30585  iundifdif  31523  nepss  34329  axextndbi  34418  ontopbas  34929  bj-elccinfty  35714  ctbssinf  35906  poimirlem16  36123  mblfinlem4  36147  ismblfin  36148  fiphp3d  41171  onmcl  41695  omabs2  41696  eelT01  43067  eel0T1  43068  un01  43145  dirkercncf  44422  nnsum3primes4  46054  line2x  46914  line2y  46915
  Copyright terms: Public domain W3C validator