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  5443  relop  5790  odi  8494  ssfi  9082  endjudisj  10057  nn0n0n1ge2  12446  0mod  13803  expge1  14003  hashge2el2dif  14384  swrdccatin2  14633  swrd2lsw  14856  4dvdseven  16281  ndvdsp1  16319  istrkg2ld  28436  0wlkons1  30096  ococin  31383  cmbr4i  31576  iundifdif  32537  wevgblacfn  35141  nepss  35750  axextndbi  35837  ontopbas  36461  bj-elccinfty  37247  ctbssinf  37439  poimirlem16  37675  mblfinlem4  37699  ismblfin  37700  fiphp3d  42851  onmcl  43363  omabs2  43364  eelT01  44742  eel0T1  44743  un01  44820  dirkercncf  46144  nnsum3primes4  47818  vopnbgrelself  47885  line2x  48785  line2y  48786