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  5766  brprcneu  6818  brprcneuALT  6819  mpoeq12  7425  tfr3  8324  oaabslem  8568  omabslem  8571  enrefnn  8975  pssnn  9085  isinf  9156  preleqALT  9514  ige2m2fzo  13630  uzindi  13891  drsdirfi  18213  ga0  19212  lbsext  21102  lindfrn  21760  toprntopon  22841  fbssint  23754  filssufilg  23827  neiflim  23890  lmmbrf  25190  caucfil  25211  lrrecfr  27887  konigsbergssiedgwpr  30231  sspid  30707  satfdmfmla  35465  satefvfmla1  35490  onsucsuccmpi  36508  bj-restn0  37155  poimirlem28  37708  lhpexle1  40127  diophun  42890  eldioph4b  42928  tfsconcatlem  43453  relexp1idm  43831  relexp0idm  43832  dvsid  44448  dvsef  44449  un10  44904  cnfex  45149  dvmptfprod  46067  squeezedltsq  47010