Theorem jctl 526

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 22	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctil 522	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanl1  698  mpanlr1  704  opeqsng  5393  relop  5721  odi  8205  endjudisj  9594  nn0n0n1ge2  11963  0mod  13271  expge1  13467  hashge2el2dif  13839  swrdccatin2  14091  swrd2lsw  14314  4dvdseven  15724  ndvdsp1  15762  istrkg2ld  26246  0wlkons1  27900  ococin  29185  cmbr4i  29378  iundifdif  30314  nepss  32948  axextndbi  33049  ontopbas  33776  bj-elccinfty  34499  ctbssinf  34690  poimirlem16  34923  mblfinlem4  34947  ismblfin  34948  fiphp3d  39436  eelT01  41065  eel0T1  41066  un01  41143  dirkercncf  42412  nnsum3primes4  43973  line2x  44761  line2y  44762