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  5451  relop  5799  odi  8507  ssfi  9100  endjudisj  10082  nn0n0n1ge2  12496  0mod  13852  expge1  14052  hashge2el2dif  14433  swrdccatin2  14682  swrd2lsw  14905  4dvdseven  16333  ndvdsp1  16371  istrkg2ld  28542  0wlkons1  30206  ococin  31494  cmbr4i  31687  iundifdif  32647  wevgblacfn  35307  nepss  35916  axextndbi  36000  ontopbas  36626  bj-elccinfty  37544  ctbssinf  37736  poimirlem16  37971  mblfinlem4  37995  ismblfin  37996  fiphp3d  43265  onmcl  43777  omabs2  43778  eelT01  45155  eel0T1  45156  un01  45233  dirkercncf  46553  nnsum3primes4  48276  vopnbgrelself  48343  line2x  49242  line2y  49243