Theorem jctl 531

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 527	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpanl1  710  mpanlr1  716  opeqsng  5471  relop  5820  odi  8543  ssfi  9137  endjudisj  10122  nn0n0n1ge2  12546  0mod  13909  expge1  14109  hashge2el2dif  14490  swrdccatin2  14739  swrd2lsw  14962  4dvdseven  16390  ndvdsp1  16428  istrkg2ld  28606  0wlkons1  30269  ococin  31557  cmbr4i  31750  iundifdif  32711  wevgblacfn  35418  nepss  36032  axextndbi  36116  ontopbas  36752  bj-elccinfty  37670  ctbssinf  37864  poimirlem16  38099  mblfinlem4  38123  ismblfin  38124  fiphp3d  43360  onmcl  43872  omabs2  43873  eelT01  45250  eel0T1  45251  un01  45328  dirkercncf  46645  nnsum3primes4  48374  vopnbgrelself  48441  line2x  49340  line2y  49341