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  relopabiOLD  5806  brprcneu  6898  brprcneuALT  6899  mpoeq12  7516  tfr3  8435  oaabslem  8684  omabslem  8687  enrefnn  9102  pssnn  9212  isinf  9284  preleqALT  9645  ige2m2fzo  13890  uzindi  14152  drsdirfi  18508  ga0  19542  lbsext  21471  lindfrn  22157  toprntopon  23273  fbssint  24187  filssufilg  24260  neiflim  24323  lmmbrf  25613  caucfil  25634  lrrecfr  28359  konigsbergssiedgwpr  30880  sspid  31357  satfdmfmla  36332  satefvfmla1  36357  onsucsuccmpi  37409  bj-restn0  38202  poimirlem28  38758  lhpexle1  41257  diophun  43977  eldioph4b  44011  tfsconcatlem  44530  relexp1idm  44906  relexp0idm  44907  dvsid  45507  dvsef  45508  un10  45961  cnfex  46250  dvmptfprod  47160