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  697  mpanr2  700  exan  1866  relopabi  5721  brprcneu  6747  fvprc  6748  mpoeq12  7326  tfr3  8201  oaabslem  8437  omabslem  8440  enrefnn  8791  pssnn  8913  isinf  8965  pssnnOLD  8969  preleqALT  9305  ige2m2fzo  13378  uzindi  13630  drsdirfi  17938  ga0  18819  lbsext  20340  lindfrn  20938  toprntopon  21982  fbssint  22897  filssufilg  22970  neiflim  23033  lmmbrf  24331  caucfil  24352  konigsbergssiedgwpr  28514  sspid  28988  satfdmfmla  33262  satefvfmla1  33287  lrrecfr  34027  onsucsuccmpi  34559  bj-restn0  35188  poimirlem28  35732  lhpexle1  37949  diophun  40511  eldioph4b  40549  relexp1idm  41211  relexp0idm  41212  dvsid  41838  dvsef  41839  un10  42297  cnfex  42460  dvmptfprod  43376