Theorem jctl 523

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanl1  699  mpanlr1  705  opeqsng  5522  relop  5875  odi  8635  ssfi  9240  endjudisj  10238  nn0n0n1ge2  12620  0mod  13953  expge1  14150  hashge2el2dif  14529  swrdccatin2  14777  swrd2lsw  15001  4dvdseven  16421  ndvdsp1  16459  istrkg2ld  28486  0wlkons1  30153  ococin  31440  cmbr4i  31633  iundifdif  32585  wevgblacfn  35076  nepss  35680  axextndbi  35768  ontopbas  36394  bj-elccinfty  37180  ctbssinf  37372  poimirlem16  37596  mblfinlem4  37620  ismblfin  37621  fiphp3d  42775  onmcl  43293  omabs2  43294  eelT01  44682  eel0T1  44683  un01  44760  dirkercncf  46028  nnsum3primes4  47662  vopnbgrelself  47727  line2x  48488  line2y  48489