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  1860  relopabi  5835  brprcneu  6897  brprcneuALT  6898  mpoeq12  7506  tfr3  8438  oaabslem  8684  omabslem  8687  enrefnn  9086  pssnn  9207  isinf  9294  isinfOLD  9295  preleqALT  9655  ige2m2fzo  13764  uzindi  14020  drsdirfi  18363  ga0  19329  lbsext  21183  lindfrn  21859  toprntopon  22947  fbssint  23862  filssufilg  23935  neiflim  23998  lmmbrf  25310  caucfil  25331  lrrecfr  27991  konigsbergssiedgwpr  30278  sspid  30754  satfdmfmla  35385  satefvfmla1  35410  onsucsuccmpi  36426  bj-restn0  37073  poimirlem28  37635  lhpexle1  39991  diophun  42761  eldioph4b  42799  tfsconcatlem  43326  relexp1idm  43704  relexp0idm  43705  dvsid  44327  dvsef  44328  un10  44786  cnfex  44966  dvmptfprod  45901