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  701  mpanlr1  707  opeqsng  5457  relop  5805  odi  8514  ssfi  9107  endjudisj  10091  nn0n0n1ge2  12505  0mod  13861  expge1  14061  hashge2el2dif  14442  swrdccatin2  14691  swrd2lsw  14914  4dvdseven  16342  ndvdsp1  16380  istrkg2ld  28528  0wlkons1  30191  ococin  31479  cmbr4i  31672  iundifdif  32632  wevgblacfn  35291  nepss  35900  axextndbi  35984  ontopbas  36610  bj-elccinfty  37528  ctbssinf  37722  poimirlem16  37957  mblfinlem4  37981  ismblfin  37982  fiphp3d  43247  onmcl  43759  omabs2  43760  eelT01  45137  eel0T1  45138  un01  45215  dirkercncf  46535  nnsum3primes4  48264  vopnbgrelself  48331  line2x  49230  line2y  49231