Theorem jctr 534

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanl2  714  mpanr2  717  exan  1895  relopabi  5800  brprcneu  6867  brprcneuALT  6868  mpoeq12  7485  tfr3  8391  oaabslem  8640  omabslem  8643  enrefnn  9058  pssnn  9168  isinf  9240  preleqALT  9602  ige2m2fzo  13843  uzindi  14105  drsdirfi  18459  ga0  19492  lbsext  21421  lindfrn  22107  toprntopon  23223  fbssint  24137  filssufilg  24210  neiflim  24273  lmmbrf  25563  caucfil  25584  lrrecfr  28311  konigsbergssiedgwpr  30832  sspid  31309  satfdmfmla  36134  satefvfmla1  36159  onsucsuccmpi  37201  bj-restn0  37979  poimirlem28  38534  lhpexle1  41033  diophun  43737  eldioph4b  43771  tfsconcatlem  44296  relexp1idm  44673  relexp0idm  44674  dvsid  45274  dvsef  45275  un10  45729  cnfex  45988  dvmptfprod  46899