Theorem jctr 525

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 521	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanl2  698  mpanr2  701  exan  1866  relopabi  5734  brprcneu  6773  brprcneuALT  6774  mpoeq12  7357  tfr3  8239  oaabslem  8486  omabslem  8489  enrefnn  8846  pssnn  8960  isinf  9045  pssnnOLD  9049  preleqALT  9384  ige2m2fzo  13459  uzindi  13711  drsdirfi  18032  ga0  18913  lbsext  20434  lindfrn  21037  toprntopon  22083  fbssint  22998  filssufilg  23071  neiflim  23134  lmmbrf  24435  caucfil  24456  konigsbergssiedgwpr  28622  sspid  29096  satfdmfmla  33371  satefvfmla1  33396  lrrecfr  34109  onsucsuccmpi  34641  bj-restn0  35270  poimirlem28  35814  lhpexle1  38029  diophun  40602  eldioph4b  40640  relexp1idm  41329  relexp0idm  41330  dvsid  41956  dvsef  41957  un10  42415  cnfex  42578  dvmptfprod  43493