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  5488  relop  5838  odi  8565  ssfi  9158  endjudisj  10153  nn0n0n1ge2  12573  0mod  13937  expge1  14137  hashge2el2dif  14519  swrdccatin2  14768  swrd2lsw  14991  4dvdseven  16432  ndvdsp1  16470  istrkg2ld  28707  0wlkons1  30450  ococin  31738  cmbr4i  31931  iundifdif  32885  wevgblacfn  35573  nepss  36188  axextndbi  36272  ontopbas  36917  bj-elccinfty  37836  ctbssinf  38030  poimirlem16  38265  mblfinlem4  38289  ismblfin  38290  fiphp3d  43526  onmcl  44038  omabs2  44039  eelT01  45399  eel0T1  45400  un01  45477  dirkercncf  46801  nnsum3primes4  48530  vopnbgrelself  48597  line2x  49511  line2y  49512