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

This theorem is referenced by:  mpanl1  696  mpanlr1  702  opeqsng  5411  relop  5748  odi  8372  ssfi  8918  endjudisj  9855  nn0n0n1ge2  12230  0mod  13550  expge1  13748  hashge2el2dif  14122  swrdccatin2  14370  swrd2lsw  14593  4dvdseven  16010  ndvdsp1  16048  istrkg2ld  26725  0wlkons1  28386  ococin  29671  cmbr4i  29864  iundifdif  30803  nepss  33564  axextndbi  33686  ontopbas  34544  bj-elccinfty  35312  ctbssinf  35504  poimirlem16  35720  mblfinlem4  35744  ismblfin  35745  fiphp3d  40557  eelT01  42220  eel0T1  42221  un01  42298  dirkercncf  43538  nnsum3primes4  45128  line2x  45988  line2y  45989