Theorem jctl 523

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanl1  700  mpanlr1  706  opeqsng  5466  relop  5817  odi  8546  ssfi  9143  endjudisj  10129  nn0n0n1ge2  12517  0mod  13871  expge1  14071  hashge2el2dif  14452  swrdccatin2  14701  swrd2lsw  14925  4dvdseven  16350  ndvdsp1  16388  istrkg2ld  28394  0wlkons1  30057  ococin  31344  cmbr4i  31537  iundifdif  32498  wevgblacfn  35103  nepss  35712  axextndbi  35799  ontopbas  36423  bj-elccinfty  37209  ctbssinf  37401  poimirlem16  37637  mblfinlem4  37661  ismblfin  37662  fiphp3d  42814  onmcl  43327  omabs2  43328  eelT01  44707  eel0T1  44708  un01  44785  dirkercncf  46112  nnsum3primes4  47793  vopnbgrelself  47859  line2x  48747  line2y  48748