Theorem jctl 563

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  mpanl1  716  mpanlr1  722  relop  5305  odi  7704  cdaun  9032  nn0n0n1ge2  11396  0mod  12741  expge1  12937  hashge2el2dif  13300  swrd2lsw  13741  4dvdseven  15156  ndvdsp1  15182  istrkg2ld  25404  wspthsnwspthsnonOLD  26881  0wlkons1  27099  ococin  28395  cmbr4i  28588  iundifdif  29507  nepss  31725  axextndbi  31834  ontopbas  32552  bj-elccinfty  33231  poimirlem16  33555  mblfinlem4  33579  ismblfin  33580  fiphp3d  37700  eelT01  39253  eel0T1  39254  un01  39333  dirkercncf  40642  nnsum3primes4  42001