Theorem jctr 532

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 22	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctir 528	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mpanl2  711  mpanr2  714  exan  1881  just3-df  2087  relopabi  5793  brprcneu  6853  brprcneuALT  6854  mpoeq12  7465  tfr3  8365  oaabslem  8612  omabslem  8615  enrefnn  9023  pssnn  9133  isinf  9205  preleqALT  9569  ige2m2fzo  13731  uzindi  13992  drsdirfi  18320  ga0  19321  lbsext  21213  lindfrn  21853  toprntopon  22965  fbssint  23878  filssufilg  23951  neiflim  24014  lmmbrf  25304  caucfil  25325  lrrecfr  28013  konigsbergssiedgwpr  30397  sspid  30874  satfdmfmla  35714  satefvfmla1  35739  onsucsuccmpi  36767  bj-restn0  37544  poimirlem28  38111  lhpexle1  40596  diophun  43318  eldioph4b  43352  tfsconcatlem  43877  relexp1idm  44254  relexp0idm  44255  dvsid  44871  dvsef  44872  un10  45327  cnfex  45572  dvmptfprod  46483  squeezedltsq  47428