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  700  mpanr2  703  exan  1863  relopabi  5658  brprcneu  6637  mpoeq12  7206  tfr3  8018  oaabslem  8253  omabslem  8256  isinf  8715  pssnn  8720  preleqALT  9064  ige2m2fzo  13095  uzindi  13345  drsdirfi  17540  ga0  18420  lbsext  19928  lindfrn  20510  toprntopon  21530  fbssint  22443  filssufilg  22516  neiflim  22579  lmmbrf  23866  caucfil  23887  konigsbergssiedgwpr  28034  sspid  28508  satfdmfmla  32760  satefvfmla1  32785  onsucsuccmpi  33904  bj-restn0  34505  poimirlem28  35085  lhpexle1  37304  diophun  39714  eldioph4b  39752  relexp1idm  40415  relexp0idm  40416  dvsid  41035  dvsef  41036  un10  41494  cnfex  41657  dvmptfprod  42587