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  5483  relop  5835  odi  8596  ssfi  9192  endjudisj  10188  nn0n0n1ge2  12574  0mod  13924  expge1  14122  hashge2el2dif  14503  swrdccatin2  14752  swrd2lsw  14976  4dvdseven  16397  ndvdsp1  16435  istrkg2ld  28444  0wlkons1  30107  ococin  31394  cmbr4i  31587  iundifdif  32548  wevgblacfn  35136  nepss  35740  axextndbi  35827  ontopbas  36451  bj-elccinfty  37237  ctbssinf  37429  poimirlem16  37665  mblfinlem4  37689  ismblfin  37690  fiphp3d  42809  onmcl  43322  omabs2  43323  eelT01  44702  eel0T1  44703  un01  44780  dirkercncf  46103  nnsum3primes4  47769  vopnbgrelself  47835  line2x  48701  line2y  48702