Theorem jctr 533

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctir 529	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanl2  713  mpanr2  716  exan  1885  just3-df  2091  relopabi  5800  brprcneu  6861  brprcneuALT  6862  mpoeq12  7473  tfr3  8374  oaabslem  8621  omabslem  8624  enrefnn  9031  pssnn  9141  isinf  9213  preleqALT  9574  ige2m2fzo  13748  uzindi  14009  drsdirfi  18351  ga0  19359  lbsext  21256  lindfrn  21931  toprntopon  23043  fbssint  23956  filssufilg  24029  neiflim  24092  lmmbrf  25382  caucfil  25403  lrrecfr  28094  konigsbergssiedgwpr  30509  sspid  30986  satfdmfmla  35763  satefvfmla1  35788  onsucsuccmpi  36816  bj-restn0  37592  poimirlem28  38159  lhpexle1  40644  diophun  43366  eldioph4b  43400  tfsconcatlem  43925  relexp1idm  44302  relexp0idm  44303  dvsid  44905  dvsef  44906  un10  45361  cnfex  45606  dvmptfprod  46517  squeezedltsq  47462