Theorem jctr 527

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanl2  699  mpanr2  702  exan  1862  exanOLD  1863  relopabi  5694  brprcneu  6662  mpoeq12  7227  tfr3  8035  oaabslem  8270  omabslem  8273  isinf  8731  pssnn  8736  preleqALT  9080  ige2m2fzo  13101  uzindi  13351  drsdirfi  17548  ga0  18428  lbsext  19935  lindfrn  20965  toprntopon  21533  fbssint  22446  filssufilg  22519  neiflim  22582  lmmbrf  23865  caucfil  23886  konigsbergssiedgwpr  28028  sspid  28502  satfdmfmla  32647  satefvfmla1  32672  onsucsuccmpi  33791  bj-restn0  34384  poimirlem28  34935  lhpexle1  37159  diophun  39390  eldioph4b  39428  relexp1idm  40079  relexp0idm  40080  dvsid  40683  dvsef  40684  un10  41142  cnfex  41305  dvmptfprod  42250