Theorem jctr 524

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 520	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanl2  701  mpanr2  704  exan  1862  relopabi  5769  brprcneu  6816  brprcneuALT  6817  mpoeq12  7426  tfr3  8328  oaabslem  8572  omabslem  8575  enrefnn  8979  pssnn  9092  isinf  9165  isinfOLD  9166  preleqALT  9532  ige2m2fzo  13649  uzindi  13907  drsdirfi  18229  ga0  19195  lbsext  21088  lindfrn  21746  toprntopon  22828  fbssint  23741  filssufilg  23814  neiflim  23877  lmmbrf  25178  caucfil  25199  lrrecfr  27873  konigsbergssiedgwpr  30211  sspid  30687  satfdmfmla  35372  satefvfmla1  35397  onsucsuccmpi  36416  bj-restn0  37063  poimirlem28  37627  lhpexle1  39987  diophun  42746  eldioph4b  42784  tfsconcatlem  43309  relexp1idm  43687  relexp0idm  43688  dvsid  44304  dvsef  44305  un10  44761  cnfex  45006  dvmptfprod  45927  squeezedltsq  46871