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  1861  relopabi  5831  brprcneu  6895  brprcneuALT  6896  mpoeq12  7507  tfr3  8440  oaabslem  8686  omabslem  8689  enrefnn  9088  pssnn  9209  isinf  9297  isinfOLD  9298  preleqALT  9658  ige2m2fzo  13768  uzindi  14024  drsdirfi  18352  ga0  19317  lbsext  21166  lindfrn  21842  toprntopon  22932  fbssint  23847  filssufilg  23920  neiflim  23983  lmmbrf  25297  caucfil  25318  lrrecfr  27977  konigsbergssiedgwpr  30269  sspid  30745  satfdmfmla  35406  satefvfmla1  35431  onsucsuccmpi  36445  bj-restn0  37092  poimirlem28  37656  lhpexle1  40011  diophun  42789  eldioph4b  42827  tfsconcatlem  43354  relexp1idm  43732  relexp0idm  43733  dvsid  44355  dvsef  44356  un10  44813  cnfex  45038  dvmptfprod  45965