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  5459  relop  5807  odi  8516  ssfi  9109  endjudisj  10091  nn0n0n1ge2  12481  0mod  13834  expge1  14034  hashge2el2dif  14415  swrdccatin2  14664  swrd2lsw  14887  4dvdseven  16312  ndvdsp1  16350  istrkg2ld  28544  0wlkons1  30208  ococin  31495  cmbr4i  31688  iundifdif  32648  wevgblacfn  35322  nepss  35931  axextndbi  36015  ontopbas  36641  bj-elccinfty  37463  ctbssinf  37655  poimirlem16  37881  mblfinlem4  37905  ismblfin  37906  fiphp3d  43170  onmcl  43682  omabs2  43683  eelT01  45060  eel0T1  45061  un01  45138  dirkercncf  46459  nnsum3primes4  48142  vopnbgrelself  48209  line2x  49108  line2y  49109