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  5503  relop  5850  odi  8581  ssfi  9175  endjudisj  10165  nn0n0n1ge2  12541  0mod  13869  expge1  14067  hashge2el2dif  14443  swrdccatin2  14681  swrd2lsw  14905  4dvdseven  16318  ndvdsp1  16356  istrkg2ld  27749  0wlkons1  29412  ococin  30699  cmbr4i  30892  iundifdif  31832  nepss  34762  axextndbi  34851  ontopbas  35405  bj-elccinfty  36187  ctbssinf  36379  poimirlem16  36596  mblfinlem4  36620  ismblfin  36621  fiphp3d  41645  onmcl  42169  omabs2  42170  eelT01  43560  eel0T1  43561  un01  43638  dirkercncf  44908  nnsum3primes4  46541  line2x  47524  line2y  47525