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

Theorem jctl 524
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 520 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpanl1  696  mpanlr1  702  opeqsng  5384  relop  5714  odi  8194  endjudisj  9582  nn0n0n1ge2  11950  0mod  13258  expge1  13454  hashge2el2dif  13826  swrdccatin2  14079  swrd2lsw  14302  4dvdseven  15712  ndvdsp1  15750  istrkg2ld  26173  0wlkons1  27827  ococin  29112  cmbr4i  29305  iundifdif  30242  nepss  32845  axextndbi  32946  ontopbas  33673  bj-elccinfty  34388  ctbssinf  34569  poimirlem16  34789  mblfinlem4  34813  ismblfin  34814  fiphp3d  39294  eelT01  40922  eel0T1  40923  un01  41000  dirkercncf  42269  nnsum3primes4  43830  line2x  44669  line2y  44670
  Copyright terms: Public domain W3C validator