Theorem jctr 565

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  mpanl2  717  mpanr2  720  relopabi  5245  brprcneu  6184  mpt2eq12  6715  tfr3  7495  oaabslem  7723  omabslem  7726  isinf  8173  pssnn  8178  ige2m2fzo  12530  uzindi  12781  drsdirfi  16938  ga0  17731  lbsext  19163  lindfrn  20160  toprntopon  20729  fbssint  21642  filssufilg  21715  neiflim  21778  lmmbrf  23060  caucfil  23081  konigsbergssiedgwpr  27110  sspid  27580  onsucsuccmpi  32442  bj-restsn0  33038  bj-restn0  33043  poimirlem28  33437  lhpexle1  35294  diophun  37337  eldioph4b  37375  relexp1idm  38006  relexp0idm  38007  dvsid  38530  dvsef  38531  un10  39015  cnfex  39187  dvmptfprod  40160