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  1863  relopabi  5762  brprcneu  6812  brprcneuALT  6813  mpoeq12  7419  tfr3  8318  oaabslem  8562  omabslem  8565  enrefnn  8968  pssnn  9078  isinf  9149  preleqALT  9507  ige2m2fzo  13625  uzindi  13886  drsdirfi  18208  ga0  19208  lbsext  21098  lindfrn  21756  toprntopon  22838  fbssint  23751  filssufilg  23824  neiflim  23887  lmmbrf  25187  caucfil  25208  lrrecfr  27884  konigsbergssiedgwpr  30224  sspid  30700  satfdmfmla  35432  satefvfmla1  35457  onsucsuccmpi  36476  bj-restn0  37123  poimirlem28  37687  lhpexle1  40046  diophun  42805  eldioph4b  42843  tfsconcatlem  43368  relexp1idm  43746  relexp0idm  43747  dvsid  44363  dvsef  44364  un10  44819  cnfex  45064  dvmptfprod  45982  squeezedltsq  46916