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  5507  relop  5860  odi  8618  ssfi  9214  endjudisj  10210  nn0n0n1ge2  12596  0mod  13943  expge1  14141  hashge2el2dif  14520  swrdccatin2  14768  swrd2lsw  14992  4dvdseven  16411  ndvdsp1  16449  istrkg2ld  28469  0wlkons1  30141  ococin  31428  cmbr4i  31621  iundifdif  32576  wevgblacfn  35115  nepss  35719  axextndbi  35806  ontopbas  36430  bj-elccinfty  37216  ctbssinf  37408  poimirlem16  37644  mblfinlem4  37668  ismblfin  37669  fiphp3d  42835  onmcl  43349  omabs2  43350  eelT01  44736  eel0T1  44737  un01  44814  dirkercncf  46127  nnsum3primes4  47780  vopnbgrelself  47846  line2x  48680  line2y  48681