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  702  mpanr2  705  exan  1864  relopabi  5779  brprcneu  6832  brprcneuALT  6833  mpoeq12  7441  tfr3  8340  oaabslem  8585  omabslem  8588  enrefnn  8995  pssnn  9105  isinf  9177  preleqALT  9538  ige2m2fzo  13656  uzindi  13917  drsdirfi  18240  ga0  19239  lbsext  21130  lindfrn  21788  toprntopon  22881  fbssint  23794  filssufilg  23867  neiflim  23930  lmmbrf  25230  caucfil  25251  lrrecfr  27951  konigsbergssiedgwpr  30336  sspid  30812  satfdmfmla  35613  satefvfmla1  35638  onsucsuccmpi  36656  bj-restn0  37337  poimirlem28  37893  lhpexle1  40378  diophun  43124  eldioph4b  43162  tfsconcatlem  43687  relexp1idm  44064  relexp0idm  44065  dvsid  44681  dvsef  44682  un10  45137  cnfex  45382  dvmptfprod  46297  squeezedltsq  47240