Theorem jctl 561

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  mpanl1  711  mpanlr1  717  relop  5182  odi  7523  cdaun  8854  nn0n0n1ge2  11205  0mod  12518  expge1  12714  hashge2el2dif  13067  swrd2lsw  13489  4dvdseven  14893  ndvdsp1  14919  istrkg2ld  25076  cusgra3vnbpr  25760  constr2spthlem1  25890  2pthon  25898  constr3trllem2  25945  constr3pthlem1  25949  constr3pthlem2  25950  wlkiswwlk2  25991  ococin  27457  cmbr4i  27650  iundifdif  28569  nepss  30660  axextndbi  30760  ontopbas  31403  bj-elccinfty  32074  poimirlem16  32391  mblfinlem4  32415  ismblfin  32416  fiphp3d  36197  eelT01  37753  eel0T1  37754  un01  37833  dirkercncf  38797  nnsum3primes4  40002  wspthsnwspthsnon  41117  0wlkOns1  41284