Theorem jctl 533

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanl1  713  mpanlr1  719  opeqsng  5475  relop  5828  odi  8571  ssfi  9172  endjudisj  10228  nn0n0n1ge2  12655  0mod  14022  expge1  14222  hashge2el2dif  14605  swrdccatin2  14858  swrd2lsw  15085  4dvdseven  16523  ndvdsp1  16561  istrkg2ld  28904  0wlkons1  30694  ococin  31992  cmbr4i  32185  iundifdif  33139  wevgblacfn  35863  nepss  36452  axextndbi  36536  ontopbas  37186  bj-elccinfty  38103  ctbssinf  38297  poimirlem16  38522  mblfinlem4  38546  ismblfin  38547  fiphp3d  43779  onmcl  44291  omabs2  44292  eelT01  45652  eel0T1  45653  un01  45730  dirkercncf  47061  nnsum3primes4  48830  vopnbgrelself  48897  line2x  49810  line2y  49811