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  5803  brprcneu  6868  brprcneuALT  6869  mpoeq12  7486  tfr3  8388  oaabslem  8635  omabslem  8638  enrefnn  9053  pssnn  9163  isinf  9235  preleqALT  9596  ige2m2fzo  13784  uzindi  14046  drsdirfi  18393  ga0  19425  lbsext  21350  lindfrn  22034  toprntopon  23150  fbssint  24064  filssufilg  24137  neiflim  24200  lmmbrf  25490  caucfil  25511  lrrecfr  28208  konigsbergssiedgwpr  30729  sspid  31206  satfdmfmla  35979  satefvfmla1  36004  onsucsuccmpi  37062  bj-restn0  37840  poimirlem28  38397  lhpexle1  40881  diophun  43618  eldioph4b  43652  tfsconcatlem  44177  relexp1idm  44554  relexp0idm  44555  dvsid  45155  dvsef  45156  un10  45610  cnfex  45862  dvmptfprod  46773