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  5463  relop  5814  odi  8543  ssfi  9137  endjudisj  10122  nn0n0n1ge2  12510  0mod  13864  expge1  14064  hashge2el2dif  14445  swrdccatin2  14694  swrd2lsw  14918  4dvdseven  16343  ndvdsp1  16381  istrkg2ld  28387  0wlkons1  30050  ococin  31337  cmbr4i  31530  iundifdif  32491  wevgblacfn  35096  nepss  35705  axextndbi  35792  ontopbas  36416  bj-elccinfty  37202  ctbssinf  37394  poimirlem16  37630  mblfinlem4  37654  ismblfin  37655  fiphp3d  42807  onmcl  43320  omabs2  43321  eelT01  44700  eel0T1  44701  un01  44778  dirkercncf  46105  nnsum3primes4  47789  vopnbgrelself  47855  line2x  48743  line2y  48744