Theorem jctl 528

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanl1  706  mpanlr1  712  opeqsng  5451  relop  5799  odi  8511  ssfi  9104  endjudisj  10089  nn0n0n1ge2  12503  0mod  13859  expge1  14059  hashge2el2dif  14440  swrdccatin2  14689  swrd2lsw  14912  4dvdseven  16340  ndvdsp1  16378  istrkg2ld  28553  0wlkons1  30216  ococin  31504  cmbr4i  31697  iundifdif  32658  wevgblacfn  35344  nepss  35953  axextndbi  36037  ontopbas  36663  bj-elccinfty  37581  ctbssinf  37775  poimirlem16  38010  mblfinlem4  38034  ismblfin  38035  fiphp3d  43271  onmcl  43783  omabs2  43784  eelT01  45161  eel0T1  45162  un01  45239  dirkercncf  46557  nnsum3primes4  48286  vopnbgrelself  48353  line2x  49252  line2y  49253