Theorem jctl 562

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpanl1  712  mpanlr1  718  relop  5194  odi  7546  cdaun  8877  nn0n0n1ge2  11235  0mod  12563  expge1  12759  hashge2el2dif  13117  swrd2lsw  13543  4dvdseven  14947  ndvdsp1  14973  istrkg2ld  25159  cusgra3vnbpr  25994  constr2spthlem1  26124  2pthon  26132  constr3trllem2  26179  constr3pthlem1  26183  constr3pthlem2  26184  wlkiswwlk2  26225  ococin  27651  cmbr4i  27844  iundifdif  28763  nepss  30854  axextndbi  30954  ontopbas  31597  bj-elccinfty  32278  poimirlem16  32595  mblfinlem4  32619  ismblfin  32620  fiphp3d  36401  eelT01  37957  eel0T1  37958  un01  38037  dirkercncf  39000  nnsum3primes4  40204  wspthsnwspthsnon  41122  0wlkOns1  41289