Theorem jctr 564

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  mpanl2  717  mpanr2  720  relopabi  5278  brprcneu  6222  mpt2eq12  6757  tfr3  7540  oaabslem  7768  omabslem  7771  isinf  8214  pssnn  8219  ige2m2fzo  12570  uzindi  12821  drsdirfi  16985  ga0  17777  lbsext  19211  lindfrn  20208  toprntopon  20777  fbssint  21689  filssufilg  21762  neiflim  21825  lmmbrf  23106  caucfil  23127  konigsbergssiedgwpr  27227  sspid  27708  onsucsuccmpi  32567  bj-restsn0  33163  bj-restn0  33168  poimirlem28  33567  lhpexle1  35612  diophun  37654  eldioph4b  37692  relexp1idm  38323  relexp0idm  38324  dvsid  38847  dvsef  38848  un10  39332  cnfex  39501  dvmptfprod  40478