Theorem jctr 521

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

Syntax hints:   → wi 4   ∧ wa 385

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

This theorem is referenced by:  mpanl2  693  mpanr2  696  exan  1958  relopabi  5449  brprcneu  6403  mpt2eq12  6949  tfr3  7734  oaabslem  7963  omabslem  7966  isinf  8415  pssnn  8420  preleqALT  8762  ige2m2fzo  12786  uzindi  13036  drsdirfi  17253  ga0  18043  lbsext  19486  lindfrn  20485  toprntopon  21058  fbssint  21970  filssufilg  22043  neiflim  22106  lmmbrf  23388  caucfil  23409  konigsbergssiedgwpr  27596  sspid  28105  onsucsuccmpi  32950  bj-restsn0  33531  bj-restn0  33536  poimirlem28  33926  lhpexle1  36029  diophun  38123  eldioph4b  38161  relexp1idm  38789  relexp0idm  38790  dvsid  39312  dvsef  39313  un10  39784  cnfex  39947  dvmptfprod  40904