Theorem jctr 525

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpanl2  699  mpanr2  702  exan  1865  relopabi  5822  brprcneu  6881  brprcneuALT  6882  mpoeq12  7484  tfr3  8401  oaabslem  8648  omabslem  8651  enrefnn  9049  pssnn  9170  isinf  9262  isinfOLD  9263  pssnnOLD  9267  preleqALT  9614  ige2m2fzo  13697  uzindi  13949  drsdirfi  18260  ga0  19164  lbsext  20782  lindfrn  21382  toprntopon  22434  fbssint  23349  filssufilg  23422  neiflim  23485  lmmbrf  24786  caucfil  24807  lrrecfr  27436  konigsbergssiedgwpr  29540  sspid  30016  satfdmfmla  34460  satefvfmla1  34485  onsucsuccmpi  35420  bj-restn0  36063  poimirlem28  36608  lhpexle1  38971  diophun  41599  eldioph4b  41637  tfsconcatlem  42174  relexp1idm  42553  relexp0idm  42554  dvsid  43178  dvsef  43179  un10  43637  cnfex  43800  dvmptfprod  44746