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

Theorem jctl 523
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 519 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mpanl1  700  mpanlr1  706  opeqsng  5507  relop  5860  odi  8618  ssfi  9214  endjudisj  10210  nn0n0n1ge2  12596  0mod  13943  expge1  14141  hashge2el2dif  14520  swrdccatin2  14768  swrd2lsw  14992  4dvdseven  16411  ndvdsp1  16449  istrkg2ld  28469  0wlkons1  30141  ococin  31428  cmbr4i  31621  iundifdif  32576  wevgblacfn  35115  nepss  35719  axextndbi  35806  ontopbas  36430  bj-elccinfty  37216  ctbssinf  37408  poimirlem16  37644  mblfinlem4  37668  ismblfin  37669  fiphp3d  42835  onmcl  43349  omabs2  43350  eelT01  44736  eel0T1  44737  un01  44814  dirkercncf  46127  nnsum3primes4  47780  vopnbgrelself  47846  line2x  48680  line2y  48681
  Copyright terms: Public domain W3C validator