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  5760  brprcneu  6807  brprcneuALT  6808  mpoeq12  7414  tfr3  8313  oaabslem  8557  omabslem  8560  enrefnn  8963  pssnn  9073  isinf  9144  preleqALT  9502  ige2m2fzo  13620  uzindi  13881  drsdirfi  18203  ga0  19203  lbsext  21093  lindfrn  21751  toprntopon  22833  fbssint  23746  filssufilg  23819  neiflim  23882  lmmbrf  25182  caucfil  25203  lrrecfr  27879  konigsbergssiedgwpr  30219  sspid  30695  satfdmfmla  35412  satefvfmla1  35437  onsucsuccmpi  36456  bj-restn0  37103  poimirlem28  37667  lhpexle1  40026  diophun  42785  eldioph4b  42823  tfsconcatlem  43348  relexp1idm  43726  relexp0idm  43727  dvsid  44343  dvsef  44344  un10  44799  cnfex  45044  dvmptfprod  45962  squeezedltsq  46896