Theorem jctl 527

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpanl1  699  mpanlr1  705  opeqsng  5358  relop  5685  odi  8188  endjudisj  9579  nn0n0n1ge2  11950  0mod  13265  expge1  13462  hashge2el2dif  13834  swrdccatin2  14082  swrd2lsw  14305  4dvdseven  15714  ndvdsp1  15752  istrkg2ld  26254  0wlkons1  27906  ococin  29191  cmbr4i  29384  iundifdif  30326  nepss  33061  axextndbi  33162  ontopbas  33889  bj-elccinfty  34629  ctbssinf  34823  poimirlem16  35073  mblfinlem4  35097  ismblfin  35098  fiphp3d  39760  eelT01  41417  eel0T1  41418  un01  41495  dirkercncf  42749  nnsum3primes4  44306  line2x  45168  line2y  45169