Theorem jctr 528

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpanl2  701  mpanr2  704  exan  1870  relopabi  5692  brprcneu  6708  fvprc  6709  mpoeq12  7284  tfr3  8135  oaabslem  8372  omabslem  8375  enrefnn  8724  pssnn  8846  isinf  8891  pssnnOLD  8895  preleqALT  9232  ige2m2fzo  13305  uzindi  13555  drsdirfi  17812  ga0  18692  lbsext  20200  lindfrn  20783  toprntopon  21822  fbssint  22735  filssufilg  22808  neiflim  22871  lmmbrf  24159  caucfil  24180  konigsbergssiedgwpr  28332  sspid  28806  satfdmfmla  33075  satefvfmla1  33100  lrrecfr  33837  onsucsuccmpi  34369  bj-restn0  34996  poimirlem28  35542  lhpexle1  37759  diophun  40298  eldioph4b  40336  relexp1idm  40999  relexp0idm  41000  dvsid  41622  dvsef  41623  un10  42081  cnfex  42244  dvmptfprod  43161