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  5446  relop  5794  odi  8500  ssfi  9089  endjudisj  10067  nn0n0n1ge2  12456  0mod  13808  expge1  14008  hashge2el2dif  14389  swrdccatin2  14638  swrd2lsw  14861  4dvdseven  16286  ndvdsp1  16324  istrkg2ld  28439  0wlkons1  30103  ococin  31390  cmbr4i  31583  iundifdif  32544  wevgblacfn  35174  nepss  35783  axextndbi  35867  ontopbas  36493  bj-elccinfty  37279  ctbssinf  37471  poimirlem16  37696  mblfinlem4  37720  ismblfin  37721  fiphp3d  42936  onmcl  43448  omabs2  43449  eelT01  44827  eel0T1  44828  un01  44905  dirkercncf  46229  nnsum3primes4  47912  vopnbgrelself  47979  line2x  48879  line2y  48880