Theorem jctl 516

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpanl1  688  mpanlr1  694  opeqsng  5245  relop  5567  odi  8004  endjudisj  9390  nn0n0n1ge2  11772  0mod  13083  expge1  13279  hashge2el2dif  13647  swrd2lsw  14174  4dvdseven  15582  ndvdsp1  15620  istrkg2ld  25963  clwlkclwwlkfOLD  27533  0wlkons1  27665  ococin  28981  cmbr4i  29174  iundifdif  30100  nepss  32505  axextndbi  32607  ontopbas  33333  bj-elccinfty  34002  ctbssinf  34165  poimirlem16  34386  mblfinlem4  34410  ismblfin  34411  fiphp3d  38850  eelT01  40501  eel0T1  40502  un01  40579  dirkercncf  41855  nnsum3primes4  43353  line2x  44141  line2y  44142