Theorem jctl 524

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 520	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 206  df-an 397

This theorem is referenced by:  mpanl1  697  mpanlr1  703  opeqsng  5417  relop  5759  odi  8410  ssfi  8956  endjudisj  9924  nn0n0n1ge2  12300  0mod  13622  expge1  13820  hashge2el2dif  14194  swrdccatin2  14442  swrd2lsw  14665  4dvdseven  16082  ndvdsp1  16120  istrkg2ld  26821  0wlkons1  28485  ococin  29770  cmbr4i  29963  iundifdif  30902  nepss  33662  axextndbi  33780  ontopbas  34617  bj-elccinfty  35385  ctbssinf  35577  poimirlem16  35793  mblfinlem4  35817  ismblfin  35818  fiphp3d  40641  eelT01  42331  eel0T1  42332  un01  42409  dirkercncf  43648  nnsum3primes4  45240  line2x  46100  line2y  46101