Theorem jctl 522

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpanl1  698  mpanlr1  704  opeqsng  5501  relop  5849  odi  8601  ssfi  9204  endjudisj  10204  nn0n0n1ge2  12585  0mod  13916  expge1  14113  hashge2el2dif  14494  swrdccatin2  14732  swrd2lsw  14956  4dvdseven  16370  ndvdsp1  16408  istrkg2ld  28384  0wlkons1  30051  ococin  31338  cmbr4i  31531  iundifdif  32483  wevgblacfn  34949  nepss  35553  axextndbi  35641  ontopbas  36153  bj-elccinfty  36934  ctbssinf  37126  poimirlem16  37350  mblfinlem4  37374  ismblfin  37375  fiphp3d  42513  onmcl  43034  omabs2  43035  eelT01  44424  eel0T1  44425  un01  44502  dirkercncf  45764  nnsum3primes4  47396  vopnbgrelself  47458  line2x  48178  line2y  48179