Theorem jctr 533

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanl2  713  mpanr2  716  exan  1892  relopabi  5811  brprcneu  6873  brprcneuALT  6874  mpoeq12  7485  tfr3  8387  oaabslem  8634  omabslem  8637  enrefnn  9044  pssnn  9154  isinf  9226  preleqALT  9587  ige2m2fzo  13759  uzindi  14020  drsdirfi  18362  ga0  19369  lbsext  21268  lindfrn  21952  toprntopon  23063  fbssint  23976  filssufilg  24049  neiflim  24112  lmmbrf  25402  caucfil  25423  lrrecfr  28114  konigsbergssiedgwpr  30578  sspid  31055  satfdmfmla  35870  satefvfmla1  35895  onsucsuccmpi  36932  bj-restn0  37710  poimirlem28  38277  lhpexle1  40760  diophun  43484  eldioph4b  43518  tfsconcatlem  44043  relexp1idm  44420  relexp0idm  44421  dvsid  45021  dvsef  45022  un10  45476  cnfex  45728  dvmptfprod  46639  squeezedltsq  47584