Theorem jctl 532

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 528	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanl1  712  mpanlr1  718  opeqsng  5477  relop  5827  odi  8552  ssfi  9145  endjudisj  10140  nn0n0n1ge2  12563  0mod  13926  expge1  14126  hashge2el2dif  14507  swrdccatin2  14756  swrd2lsw  14979  4dvdseven  16421  ndvdsp1  16459  istrkg2ld  28687  0wlkons1  30381  ococin  31669  cmbr4i  31862  iundifdif  32817  wevgblacfn  35466  nepss  36081  axextndbi  36165  ontopbas  36801  bj-elccinfty  37718  ctbssinf  37912  poimirlem16  38147  mblfinlem4  38171  ismblfin  38172  fiphp3d  43408  onmcl  43920  omabs2  43921  eelT01  45284  eel0T1  45285  un01  45362  dirkercncf  46679  nnsum3primes4  48408  vopnbgrelself  48475  line2x  49385  line2y  49386