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  702  mpanr2  705  exan  1864  relopabi  5778  brprcneu  6830  brprcneuALT  6831  mpoeq12  7440  tfr3  8338  oaabslem  8583  omabslem  8586  enrefnn  8993  pssnn  9103  isinf  9175  preleqALT  9538  ige2m2fzo  13683  uzindi  13944  drsdirfi  18271  ga0  19273  lbsext  21161  lindfrn  21801  toprntopon  22890  fbssint  23803  filssufilg  23876  neiflim  23939  lmmbrf  25229  caucfil  25250  lrrecfr  27935  konigsbergssiedgwpr  30319  sspid  30796  satfdmfmla  35582  satefvfmla1  35607  onsucsuccmpi  36625  bj-restn0  37402  poimirlem28  37969  lhpexle1  40454  diophun  43205  eldioph4b  43239  tfsconcatlem  43764  relexp1idm  44141  relexp0idm  44142  dvsid  44758  dvsef  44759  un10  45214  cnfex  45459  dvmptfprod  46373  squeezedltsq  47318