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  702  mpanr2  705  exan  1864  relopabi  5771  brprcneu  6824  brprcneuALT  6825  mpoeq12  7433  tfr3  8331  oaabslem  8576  omabslem  8579  enrefnn  8986  pssnn  9096  isinf  9168  preleqALT  9529  ige2m2fzo  13674  uzindi  13935  drsdirfi  18262  ga0  19264  lbsext  21153  lindfrn  21811  toprntopon  22900  fbssint  23813  filssufilg  23886  neiflim  23949  lmmbrf  25239  caucfil  25260  lrrecfr  27949  konigsbergssiedgwpr  30334  sspid  30811  satfdmfmla  35598  satefvfmla1  35623  onsucsuccmpi  36641  bj-restn0  37418  poimirlem28  37983  lhpexle1  40468  diophun  43219  eldioph4b  43257  tfsconcatlem  43782  relexp1idm  44159  relexp0idm  44160  dvsid  44776  dvsef  44777  un10  45232  cnfex  45477  dvmptfprod  46391  squeezedltsq  47334