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  5447  relop  5792  odi  8481  ssfi  9038  endjudisj  10025  nn0n0n1ge2  12401  0mod  13723  expge1  13921  hashge2el2dif  14294  swrdccatin2  14540  swrd2lsw  14764  4dvdseven  16181  ndvdsp1  16219  istrkg2ld  27110  0wlkons1  28773  ococin  30058  cmbr4i  30251  iundifdif  31189  nepss  33959  axextndbi  34063  ontopbas  34713  bj-elccinfty  35498  ctbssinf  35690  poimirlem16  35906  mblfinlem4  35930  ismblfin  35931  fiphp3d  40911  omabs2  41325  eelT01  42660  eel0T1  42661  un01  42738  dirkercncf  43992  nnsum3primes4  45599  line2x  46459  line2y  46460