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  5807  brprcneu  6872  brprcneuALT  6873  mpoeq12  7490  tfr3  8392  oaabslem  8639  omabslem  8642  enrefnn  9057  pssnn  9167  isinf  9239  preleqALT  9600  ige2m2fzo  13788  uzindi  14050  drsdirfi  18399  ga0  19431  lbsext  21356  lindfrn  22040  toprntopon  23156  fbssint  24070  filssufilg  24143  neiflim  24206  lmmbrf  25496  caucfil  25517  lrrecfr  28216  konigsbergssiedgwpr  30737  sspid  31214  satfdmfmla  35987  satefvfmla1  36012  onsucsuccmpi  37070  bj-restn0  37848  poimirlem28  38405  lhpexle1  40889  diophun  43626  eldioph4b  43660  tfsconcatlem  44185  relexp1idm  44562  relexp0idm  44563  dvsid  45163  dvsef  45164  un10  45618  cnfex  45870  dvmptfprod  46781