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  5491  relop  5841  odi  8573  ssfi  9167  endjudisj  10171  nn0n0n1ge2  12590  0mod  13955  expge1  14155  hashge2el2dif  14537  swrdccatin2  14790  swrd2lsw  15015  4dvdseven  16456  ndvdsp1  16494  istrkg2ld  28766  0wlkons1  30509  ococin  31797  cmbr4i  31990  iundifdif  32944  wevgblacfn  35619  nepss  36231  axextndbi  36315  ontopbas  36980  bj-elccinfty  37899  ctbssinf  38093  poimirlem16  38328  mblfinlem4  38352  ismblfin  38353  fiphp3d  43587  onmcl  44099  omabs2  44100  eelT01  45460  eel0T1  45461  un01  45538  dirkercncf  46862  nnsum3primes4  48594  vopnbgrelself  48661  line2x  49575  line2y  49576