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  1894  relopabi  5799  brprcneu  6875  brprcneuALT  6876  mpoeq12  7493  tfr3  8410  oaabslem  8659  omabslem  8662  enrefnn  9077  pssnn  9187  isinf  9259  preleqALT  9621  ige2m2fzo  13866  uzindi  14128  drsdirfi  18484  ga0  19517  lbsext  21446  lindfrn  22132  toprntopon  23248  fbssint  24162  filssufilg  24235  neiflim  24298  lmmbrf  25588  caucfil  25609  lrrecfr  28334  konigsbergssiedgwpr  30855  sspid  31332  satfdmfmla  36251  satefvfmla1  36276  onsucsuccmpi  37323  bj-restn0  38103  poimirlem28  38659  lhpexle1  41158  diophun  43877  eldioph4b  43911  tfsconcatlem  44431  relexp1idm  44807  relexp0idm  44808  dvsid  45408  dvsef  45409  un10  45863  cnfex  46138  dvmptfprod  47048