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  5785  brprcneu  6848  brprcneuALT  6849  mpoeq12  7462  tfr3  8367  oaabslem  8611  omabslem  8614  enrefnn  9018  pssnn  9132  isinf  9207  isinfOLD  9208  preleqALT  9570  ige2m2fzo  13689  uzindi  13947  drsdirfi  18266  ga0  19230  lbsext  21073  lindfrn  21730  toprntopon  22812  fbssint  23725  filssufilg  23798  neiflim  23861  lmmbrf  25162  caucfil  25183  lrrecfr  27850  konigsbergssiedgwpr  30178  sspid  30654  satfdmfmla  35387  satefvfmla1  35412  onsucsuccmpi  36431  bj-restn0  37078  poimirlem28  37642  lhpexle1  40002  diophun  42761  eldioph4b  42799  tfsconcatlem  43325  relexp1idm  43703  relexp0idm  43704  dvsid  44320  dvsef  44321  un10  44777  cnfex  45022  dvmptfprod  45943  squeezedltsq  46887