Theorem jctr 563

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpanl2  713  mpanr2  716  relopabi  5167  brprcneu  6096  mpt2eq12  6613  tfr3  7382  oaabslem  7610  omabslem  7613  isinf  8058  pssnn  8063  ige2m2fzo  12398  uzindi  12643  drsdirfi  16761  ga0  17554  lbsext  18984  lindfrn  19979  fbssint  21452  filssufilg  21525  neiflim  21588  lmmbrf  22868  caucfil  22889  constr2spth  26130  constr2pth  26131  constr3lem4  26175  sspid  26964  onsucsuccmpi  31612  bj-restsn0  32219  bj-restn0  32224  bj-toprntopon  32244  poimirlem28  32607  lhpexle1  34312  diophun  36355  eldioph4b  36393  relexp1idm  37025  relexp0idm  37026  dvsid  37552  dvsef  37553  un10  38036  cnfex  38210  dvmptfprod  38835  konigsbergssiedgwpr  41418