Theorem jctl 533

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctil 529	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanl1  713  mpanlr1  719  opeqsng  5484  relop  5834  odi  8570  ssfi  9171  endjudisj  10175  nn0n0n1ge2  12600  0mod  13967  expge1  14167  hashge2el2dif  14549  swrdccatin2  14802  swrd2lsw  15029  4dvdseven  16469  ndvdsp1  16507  istrkg2ld  28809  0wlkons1  30599  ococin  31897  cmbr4i  32090  iundifdif  33044  wevgblacfn  35716  nepss  36305  axextndbi  36389  ontopbas  37055  bj-elccinfty  37974  ctbssinf  38168  poimirlem16  38393  mblfinlem4  38417  ismblfin  38418  fiphp3d  43668  onmcl  44180  omabs2  44181  eelT01  45541  eel0T1  45542  un01  45619  dirkercncf  46943  nnsum3primes4  48712  vopnbgrelself  48779  line2x  49692  line2y  49693