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  1862  relopabi  5788  brprcneu  6851  brprcneuALT  6852  mpoeq12  7465  tfr3  8370  oaabslem  8614  omabslem  8617  enrefnn  9021  pssnn  9138  isinf  9214  isinfOLD  9215  preleqALT  9577  ige2m2fzo  13696  uzindi  13954  drsdirfi  18273  ga0  19237  lbsext  21080  lindfrn  21737  toprntopon  22819  fbssint  23732  filssufilg  23805  neiflim  23868  lmmbrf  25169  caucfil  25190  lrrecfr  27857  konigsbergssiedgwpr  30185  sspid  30661  satfdmfmla  35394  satefvfmla1  35419  onsucsuccmpi  36438  bj-restn0  37085  poimirlem28  37649  lhpexle1  40009  diophun  42768  eldioph4b  42806  tfsconcatlem  43332  relexp1idm  43710  relexp0idm  43711  dvsid  44327  dvsef  44328  un10  44784  cnfex  45029  dvmptfprod  45950  squeezedltsq  46894