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  700  mpanlr1  706  opeqsng  5450  relop  5797  odi  8504  ssfi  9097  endjudisj  10082  nn0n0n1ge2  12470  0mod  13824  expge1  14024  hashge2el2dif  14405  swrdccatin2  14653  swrd2lsw  14877  4dvdseven  16302  ndvdsp1  16340  istrkg2ld  28423  0wlkons1  30083  ococin  31370  cmbr4i  31563  iundifdif  32524  wevgblacfn  35081  nepss  35690  axextndbi  35777  ontopbas  36401  bj-elccinfty  37187  ctbssinf  37379  poimirlem16  37615  mblfinlem4  37639  ismblfin  37640  fiphp3d  42792  onmcl  43304  omabs2  43305  eelT01  44684  eel0T1  44685  un01  44762  dirkercncf  46089  nnsum3primes4  47773  vopnbgrelself  47840  line2x  48740  line2y  48741