Theorem jctr 534

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		jctl.1	. 2 ⊢ 𝜓
3	1, 2	jctir 530	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanl2  714  mpanr2  717  exan  1895  relopabi  5814  brprcneu  6878  brprcneuALT  6879  mpoeq12  7496  tfr3  8395  oaabslem  8642  omabslem  8645  enrefnn  9053  pssnn  9163  isinf  9235  preleqALT  9596  ige2m2fzo  13776  uzindi  14038  drsdirfi  18386  ga0  19399  lbsext  21324  lindfrn  22008  toprntopon  23119  fbssint  24032  filssufilg  24105  neiflim  24168  lmmbrf  25458  caucfil  25479  lrrecfr  28173  konigsbergssiedgwpr  30637  sspid  31114  satfdmfmla  35913  satefvfmla1  35938  onsucsuccmpi  36995  bj-restn0  37773  poimirlem28  38340  lhpexle1  40823  diophun  43545  eldioph4b  43579  tfsconcatlem  44104  relexp1idm  44481  relexp0idm  44482  dvsid  45082  dvsef  45083  un10  45537  cnfex  45789  dvmptfprod  46700  squeezedltsq  47644