Theorem jctr 523

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpanl2  699  mpanr2  702  exan  1857  relopabi  5823  brprcneu  6884  brprcneuALT  6885  mpoeq12  7491  tfr3  8418  oaabslem  8666  omabslem  8669  enrefnn  9070  pssnn  9191  isinf  9283  isinfOLD  9284  pssnnOLD  9288  preleqALT  9640  ige2m2fzo  13727  uzindi  13979  drsdirfi  18296  ga0  19253  lbsext  21055  lindfrn  21759  toprntopon  22857  fbssint  23772  filssufilg  23845  neiflim  23908  lmmbrf  25220  caucfil  25241  lrrecfr  27890  konigsbergssiedgwpr  30115  sspid  30591  satfdmfmla  35080  satefvfmla1  35105  onsucsuccmpi  35997  bj-restn0  36639  poimirlem28  37191  lhpexle1  39550  diophun  42258  eldioph4b  42296  tfsconcatlem  42830  relexp1idm  43209  relexp0idm  43210  dvsid  43833  dvsef  43834  un10  44292  cnfex  44455  dvmptfprod  45396