Theorem jctl 524

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanl1  698  mpanlr1  704  opeqsng  5502  relop  5848  odi  8575  ssfi  9169  endjudisj  10159  nn0n0n1ge2  12535  0mod  13863  expge1  14061  hashge2el2dif  14437  swrdccatin2  14675  swrd2lsw  14899  4dvdseven  16312  ndvdsp1  16350  istrkg2ld  27700  0wlkons1  29363  ococin  30648  cmbr4i  30841  iundifdif  31781  nepss  34675  axextndbi  34764  ontopbas  35301  bj-elccinfty  36083  ctbssinf  36275  poimirlem16  36492  mblfinlem4  36516  ismblfin  36517  fiphp3d  41542  onmcl  42066  omabs2  42067  eelT01  43457  eel0T1  43458  un01  43535  dirkercncf  44809  nnsum3primes4  46442  line2x  47393  line2y  47394