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  5451  relop  5799  odi  8506  ssfi  9097  endjudisj  10079  nn0n0n1ge2  12469  0mod  13822  expge1  14022  hashge2el2dif  14403  swrdccatin2  14652  swrd2lsw  14875  4dvdseven  16300  ndvdsp1  16338  istrkg2ld  28532  0wlkons1  30196  ococin  31483  cmbr4i  31676  iundifdif  32637  wevgblacfn  35303  nepss  35912  axextndbi  35996  ontopbas  36622  bj-elccinfty  37415  ctbssinf  37607  poimirlem16  37833  mblfinlem4  37857  ismblfin  37858  fiphp3d  43057  onmcl  43569  omabs2  43570  eelT01  44947  eel0T1  44948  un01  45025  dirkercncf  46347  nnsum3primes4  48030  vopnbgrelself  48097  line2x  48996  line2y  48997