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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctil 519	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

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  5513  relop  5864  odi  8616  ssfi  9212  endjudisj  10207  nn0n0n1ge2  12592  0mod  13939  expge1  14137  hashge2el2dif  14516  swrdccatin2  14764  swrd2lsw  14988  4dvdseven  16407  ndvdsp1  16445  istrkg2ld  28483  0wlkons1  30150  ococin  31437  cmbr4i  31630  iundifdif  32583  wevgblacfn  35093  nepss  35698  axextndbi  35786  ontopbas  36411  bj-elccinfty  37197  ctbssinf  37389  poimirlem16  37623  mblfinlem4  37647  ismblfin  37648  fiphp3d  42807  onmcl  43321  omabs2  43322  eelT01  44709  eel0T1  44710  un01  44787  dirkercncf  46063  nnsum3primes4  47713  vopnbgrelself  47779  line2x  48604  line2y  48605