Theorem jctl 530

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 526	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanl1  708  mpanlr1  714  opeqsng  5462  relop  5811  odi  8532  ssfi  9126  endjudisj  10111  nn0n0n1ge2  12535  0mod  13898  expge1  14098  hashge2el2dif  14479  swrdccatin2  14728  swrd2lsw  14951  4dvdseven  16379  ndvdsp1  16417  istrkg2ld  28595  0wlkons1  30258  ococin  31546  cmbr4i  31739  iundifdif  32700  wevgblacfn  35397  nepss  36006  axextndbi  36090  ontopbas  36726  bj-elccinfty  37644  ctbssinf  37838  poimirlem16  38073  mblfinlem4  38097  ismblfin  38098  fiphp3d  43334  onmcl  43846  omabs2  43847  eelT01  45224  eel0T1  45225  un01  45302  dirkercncf  46619  nnsum3primes4  48348  vopnbgrelself  48415  line2x  49314  line2y  49315