Theorem jctr 529

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 525	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 208  df-an 397

This theorem is referenced by:  mpanl2  707  mpanr2  710  exan  1869  relopabi  5772  brprcneu  6824  brprcneuALT  6825  mpoeq12  7436  tfr3  8335  oaabslem  8580  omabslem  8583  enrefnn  8990  pssnn  9100  isinf  9172  preleqALT  9536  ige2m2fzo  13681  uzindi  13942  drsdirfi  18269  ga0  19271  lbsext  21163  lindfrn  21803  toprntopon  22915  fbssint  23828  filssufilg  23901  neiflim  23964  lmmbrf  25254  caucfil  25275  lrrecfr  27960  konigsbergssiedgwpr  30344  sspid  30821  satfdmfmla  35635  satefvfmla1  35660  onsucsuccmpi  36678  bj-restn0  37455  poimirlem28  38022  lhpexle1  40507  diophun  43229  eldioph4b  43263  tfsconcatlem  43788  relexp1idm  44165  relexp0idm  44166  dvsid  44782  dvsef  44783  un10  45238  cnfex  45483  dvmptfprod  46395  squeezedltsq  47340