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  700  mpanr2  703  exan  1861  relopabi  5846  brprcneu  6910  brprcneuALT  6911  mpoeq12  7523  tfr3  8455  oaabslem  8703  omabslem  8706  enrefnn  9113  pssnn  9234  isinf  9323  isinfOLD  9324  preleqALT  9686  ige2m2fzo  13779  uzindi  14033  drsdirfi  18375  ga0  19338  lbsext  21188  lindfrn  21864  toprntopon  22952  fbssint  23867  filssufilg  23940  neiflim  24003  lmmbrf  25315  caucfil  25336  lrrecfr  27994  konigsbergssiedgwpr  30281  sspid  30757  satfdmfmla  35368  satefvfmla1  35393  onsucsuccmpi  36409  bj-restn0  37056  poimirlem28  37608  lhpexle1  39965  diophun  42729  eldioph4b  42767  tfsconcatlem  43298  relexp1idm  43676  relexp0idm  43677  dvsid  44300  dvsef  44301  un10  44759  cnfex  44928  dvmptfprod  45866