Theorem jctr 566

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 562	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 197  df-an 385

This theorem is referenced by:  mpanl2  719  mpanr2  722  relopabi  5393  brprcneu  6337  mpt2eq12  6872  tfr3  7656  oaabslem  7884  omabslem  7887  isinf  8330  pssnn  8335  preleqALT  8677  ige2m2fzo  12717  uzindi  12967  drsdirfi  17131  ga0  17923  lbsext  19357  lindfrn  20354  toprntopon  20923  fbssint  21835  filssufilg  21908  neiflim  21971  lmmbrf  23252  caucfil  23273  konigsbergssiedgwpr  27393  sspid  27881  onsucsuccmpi  32740  bj-restsn0  33336  bj-restn0  33341  poimirlem28  33742  lhpexle1  35789  diophun  37831  eldioph4b  37869  relexp1idm  38500  relexp0idm  38501  dvsid  39024  dvsef  39025  un10  39509  cnfex  39678  dvmptfprod  40655