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  1863  relopabi  5771  brprcneu  6824  brprcneuALT  6825  mpoeq12  7431  tfr3  8330  oaabslem  8575  omabslem  8578  enrefnn  8983  pssnn  9093  isinf  9165  preleqALT  9526  ige2m2fzo  13644  uzindi  13905  drsdirfi  18228  ga0  19227  lbsext  21118  lindfrn  21776  toprntopon  22869  fbssint  23782  filssufilg  23855  neiflim  23918  lmmbrf  25218  caucfil  25239  lrrecfr  27939  konigsbergssiedgwpr  30324  sspid  30800  satfdmfmla  35594  satefvfmla1  35619  onsucsuccmpi  36637  bj-restn0  37291  poimirlem28  37845  lhpexle1  40264  diophun  43011  eldioph4b  43049  tfsconcatlem  43574  relexp1idm  43951  relexp0idm  43952  dvsid  44568  dvsef  44569  un10  45024  cnfex  45269  dvmptfprod  46185  squeezedltsq  47128