Theorem jctr 525

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanl2  699  mpanr2  702  exan  1865  relopabi  5822  brprcneu  6881  brprcneuALT  6882  mpoeq12  7481  tfr3  8398  oaabslem  8645  omabslem  8648  enrefnn  9046  pssnn  9167  isinf  9259  isinfOLD  9260  pssnnOLD  9264  preleqALT  9611  ige2m2fzo  13694  uzindi  13946  drsdirfi  18257  ga0  19161  lbsext  20775  lindfrn  21375  toprntopon  22426  fbssint  23341  filssufilg  23414  neiflim  23477  lmmbrf  24778  caucfil  24799  lrrecfr  27424  konigsbergssiedgwpr  29499  sspid  29973  satfdmfmla  34386  satefvfmla1  34411  onsucsuccmpi  35323  bj-restn0  35966  poimirlem28  36511  lhpexle1  38874  diophun  41501  eldioph4b  41539  tfsconcatlem  42076  relexp1idm  42455  relexp0idm  42456  dvsid  43080  dvsef  43081  un10  43539  cnfex  43702  dvmptfprod  44651