Theorem jctr 524

Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)

Hypothesis

Ref	Expression
jctl.1	⊢ 𝜓

Assertion

Ref	Expression
jctr	⊢ (𝜑 → (𝜑 ∧ 𝜓))

Proof of Theorem jctr

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctir 520	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:  mpanl2  701  mpanr2  704  exan  1862  relopabi  5806  brprcneu  6871  brprcneuALT  6872  mpoeq12  7485  tfr3  8418  oaabslem  8664  omabslem  8667  enrefnn  9066  pssnn  9187  isinf  9273  isinfOLD  9274  preleqALT  9636  ige2m2fzo  13749  uzindi  14005  drsdirfi  18322  ga0  19286  lbsext  21129  lindfrn  21786  toprntopon  22868  fbssint  23781  filssufilg  23854  neiflim  23917  lmmbrf  25219  caucfil  25240  lrrecfr  27907  konigsbergssiedgwpr  30235  sspid  30711  satfdmfmla  35427  satefvfmla1  35452  onsucsuccmpi  36466  bj-restn0  37113  poimirlem28  37677  lhpexle1  40032  diophun  42763  eldioph4b  42801  tfsconcatlem  43327  relexp1idm  43705  relexp0idm  43706  dvsid  44322  dvsef  44323  un10  44779  cnfex  45019  dvmptfprod  45941  squeezedltsq  46885