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  5479  relop  5834  odi  8615  ssfi  9216  endjudisj  10274  nn0n0n1ge2  12701  0mod  14069  expge1  14269  hashge2el2dif  14652  swrdccatin2  14906  swrd2lsw  15134  4dvdseven  16572  ndvdsp1  16610  istrkg2ld  28952  0wlkons1  30742  ococin  32040  cmbr4i  32233  iundifdif  33229  wevgblacfn  36039  nepss  36661  axextndbi  36744  ontopbas  37394  bj-elccinfty  38327  ctbssinf  38521  poimirlem16  38746  mblfinlem4  38770  ismblfin  38771  fiphp3d  44019  onmcl  44525  omabs2  44526  eelT01  45884  eel0T1  45885  un01  45962  dirkercncf  47322  nnsum3primes4  49091  vopnbgrelself  49158