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 206  df-an 396

This theorem is referenced by:  mpanl2  700  mpanr2  703  exan  1858  relopabi  5818  brprcneu  6881  brprcneuALT  6882  mpoeq12  7487  tfr3  8413  oaabslem  8661  omabslem  8664  enrefnn  9063  pssnn  9184  isinf  9276  isinfOLD  9277  pssnnOLD  9281  preleqALT  9632  ige2m2fzo  13719  uzindi  13971  drsdirfi  18288  ga0  19240  lbsext  21040  lindfrn  21742  toprntopon  22814  fbssint  23729  filssufilg  23802  neiflim  23865  lmmbrf  25177  caucfil  25198  lrrecfr  27847  konigsbergssiedgwpr  30046  sspid  30522  satfdmfmla  34946  satefvfmla1  34971  onsucsuccmpi  35863  bj-restn0  36505  poimirlem28  37056  lhpexle1  39418  diophun  42115  eldioph4b  42153  tfsconcatlem  42688  relexp1idm  43067  relexp0idm  43068  dvsid  43691  dvsef  43692  un10  44150  cnfex  44313  dvmptfprod  45256