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  5474  relop  5827  odi  8590  ssfi  9191  endjudisj  10250  nn0n0n1ge2  12677  0mod  14045  expge1  14245  hashge2el2dif  14628  swrdccatin2  14882  swrd2lsw  15110  4dvdseven  16548  ndvdsp1  16586  istrkg2ld  28927  0wlkons1  30717  ococin  32015  cmbr4i  32208  iundifdif  33204  wevgblacfn  35958  nepss  36575  axextndbi  36658  ontopbas  37308  bj-elccinfty  38228  ctbssinf  38422  poimirlem16  38647  mblfinlem4  38671  ismblfin  38672  fiphp3d  43919  onmcl  44426  omabs2  44427  eelT01  45786  eel0T1  45787  un01  45864  dirkercncf  47210  nnsum3primes4  48979  vopnbgrelself  49046